This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality Restricted quantification Restricted universal and existential quantification 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 ⊢ ( 𝜑 → 𝐴 = 𝐵 )
raleqbidv.2 ⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
Assertion
rexeqbidv ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜓 ↔ ∃ 𝑥 ∈ 𝐵 𝜒 ) )
Proof
Step
Hyp
Ref
Expression
1
raleqbidv.1 ⊢ ( 𝜑 → 𝐴 = 𝐵 )
2
raleqbidv.2 ⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
3
1
eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
4
3 2
anbi12d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝜒 ) ) )
5
4
rexbidv2 ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜓 ↔ ∃ 𝑥 ∈ 𝐵 𝜒 ) )