предикаты

[spyphy]

Путаюсь немного в этом.

Пусть есть два предиката:
$P_1(A,B) = (\forall x)(Q(x,A) \vee Q(x,B) \leftrightarrow Q(x,B))$,
$P_2(A,B) = (\forall x)(Q(x,A) \to Q(x,B))$,
где $Q(x,X)$ тоже какой то предикат (например, $x \in X$, но это не важно).
Надо показать, что истинно выражение $\forall A \forall B ( P_1(A,B) \to P_2(A,B))$.
Легко показать, что $(a \vee b) \leftrightarrow b = a \to b$.
Отсюда мы заключаем, что предикаты $Q(x,A) \vee Q(x,B) \leftrightarrow Q(x,B)$ и $Q(x,A) \to Q(x,B)$ равносильны.
Отсюда как-то должно следовать, что равносильны предикаты $P_1(A,B)$ и $P_2(A,B)$, но как это показать формально?

Я пытался сделать как-то так, но это кажется не верно, так как я не нашел такой формулы логики предикатов для переноса квантора всеобщности внутрь импликации.
$((a \vee b) \eqv b ) \to ( ( a \to b )$ является тавтологией. Тогда $(Q(x,A) \vee Q(x,B) \eqv Q(x,B) ) ~\to~ (Q(x,A) \to Q(x,B) )$
истинно при всех $x,A,B$.
Это значит, что истинно высказывание
$(\forall x)(\forall A)(\forall B) ((Q(x,A) \vee Q(x,B) \eqv Q(x,B) ) ~\to~ (Q(x,A) \to Q(x,B) ))$.
Тогда истинно
$(\forall A)(\forall B) ((\forall x)(Q(x,A) \vee Q(x,B) \eqv Q(x,B) ) ~\to~ (\forall x)(Q(x,A) \to Q(x,B) ))$ ???