Metamath Proof Explorer


Theorem ralbi12f

Description: Equality deduction for restricted universal quantification. (Contributed by Giovanni Mascellani, 10-Apr-2018)

Ref Expression
Hypotheses ralbi12f.1 _ x A
ralbi12f.2 _ x B
Assertion ralbi12f A = B x A φ ψ x A φ x B ψ

Proof

Step Hyp Ref Expression
1 ralbi12f.1 _ x A
2 ralbi12f.2 _ x B
3 ralbi x A φ ψ x A φ x A ψ
4 1 2 raleqf A = B x A ψ x B ψ
5 3 4 sylan9bbr A = B x A φ ψ x A φ x B ψ