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 ( 𝐴 = 𝐵 → ( ∃ 𝑥𝐴 𝜑 ↔ ∃ 𝑥𝐵 𝜑 ) )

Proof

Step Hyp Ref Expression
1 dfcleq ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ( 𝑥𝐴𝑥𝐵 ) )
2 anbi1 ( ( 𝑥𝐴𝑥𝐵 ) → ( ( 𝑥𝐴𝜑 ) ↔ ( 𝑥𝐵𝜑 ) ) )
3 2 alexbii ( ∀ 𝑥 ( 𝑥𝐴𝑥𝐵 ) → ( ∃ 𝑥 ( 𝑥𝐴𝜑 ) ↔ ∃ 𝑥 ( 𝑥𝐵𝜑 ) ) )
4 1 3 sylbi ( 𝐴 = 𝐵 → ( ∃ 𝑥 ( 𝑥𝐴𝜑 ) ↔ ∃ 𝑥 ( 𝑥𝐵𝜑 ) ) )
5 df-rex ( ∃ 𝑥𝐴 𝜑 ↔ ∃ 𝑥 ( 𝑥𝐴𝜑 ) )
6 df-rex ( ∃ 𝑥𝐵 𝜑 ↔ ∃ 𝑥 ( 𝑥𝐵𝜑 ) )
7 4 5 6 3bitr4g ( 𝐴 = 𝐵 → ( ∃ 𝑥𝐴 𝜑 ↔ ∃ 𝑥𝐵 𝜑 ) )