Metamath Proof Explorer


Theorem rexeqbidv

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007) Remove usage of ax-10 , ax-11 , and ax-12 and reduce distinct variable conditions. (Revised by Steven Nguyen, 30-Apr-2023)

Ref Expression
Hypotheses raleqbidv.1 φ A = B
raleqbidv.2 φ ψ χ
Assertion rexeqbidv φ x A ψ x B χ

Proof

Step Hyp Ref Expression
1 raleqbidv.1 φ A = B
2 raleqbidv.2 φ ψ χ
3 1 eleq2d φ x A x B
4 3 2 anbi12d φ x A ψ x B χ
5 4 rexbidv2 φ x A ψ x B χ