Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Restricted quantification
Restricted universal and existential quantification
rexeqbii
Metamath Proof Explorer
Description: Equality deduction for restricted existential quantifier, changing both
formula and quantifier domain. Inference form. (Contributed by David
Moews , 1-May-2017)
Ref
Expression
Hypotheses
rexeqbii.1
⊢ 𝐴 = 𝐵
rexeqbii.2
⊢ ( 𝜓 ↔ 𝜒 )
Assertion
rexeqbii
⊢ ( ∃ 𝑥 ∈ 𝐴 𝜓 ↔ ∃ 𝑥 ∈ 𝐵 𝜒 )
Proof
Step
Hyp
Ref
Expression
1
rexeqbii.1
⊢ 𝐴 = 𝐵
2
rexeqbii.2
⊢ ( 𝜓 ↔ 𝜒 )
3
1
eleq2i
⊢ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 )
4
3 2
anbi12i
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝜒 ) )
5
4
rexbii2
⊢ ( ∃ 𝑥 ∈ 𝐴 𝜓 ↔ ∃ 𝑥 ∈ 𝐵 𝜒 )