Metamath Proof Explorer


Theorem rexeq

Description: Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995) Remove usage of ax-10 , ax-11 , and ax-12 . (Revised by Steven Nguyen, 30-Apr-2023) Shorten other proofs. (Revised by Wolf Lammen, 8-Mar-2025)

Ref Expression
Assertion rexeq A = B x A φ x B φ

Proof

Step Hyp Ref Expression
1 dfcleq A = B x x A x B
2 anbi1 x A x B x A φ x B φ
3 2 alexbii x x A x B x x A φ x x B φ
4 1 3 sylbi A = B x x A φ x x B φ
5 df-rex x A φ x x A φ
6 df-rex x B φ x x B φ
7 4 5 6 3bitr4g A = B x A φ x B φ