Metamath Proof Explorer


Theorem rexeqf

Description: Equality theorem for restricted existential quantifier, with bound-variable hypotheses instead of distinct variable restrictions. See rexeq for a version based on fewer axioms. (Contributed by NM, 9-Oct-2003) (Revised by Andrew Salmon, 11-Jul-2011) (Proof shortened by Wolf Lammen, 9-Mar-2025)

Ref Expression
Hypotheses raleqf.1 _ x A
raleqf.2 _ x B
Assertion rexeqf A = B x A φ x B φ

Proof

Step Hyp Ref Expression
1 raleqf.1 _ x A
2 raleqf.2 _ x B
3 1 2 raleqf A = B x A ¬ φ x B ¬ φ
4 ralnex x A ¬ φ ¬ x A φ
5 ralnex x B ¬ φ ¬ x B φ
6 3 4 5 3bitr3g A = B ¬ x A φ ¬ x B φ
7 6 con4bid A = B x A φ x B φ