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
⊢ A = B
rexeqbii.2
⊢ ψ ↔ χ
Assertion
rexeqbii
⊢ ∃ x ∈ A ψ ↔ ∃ x ∈ B χ
Proof
Step
Hyp
Ref
Expression
1
rexeqbii.1
⊢ A = B
2
rexeqbii.2
⊢ ψ ↔ χ
3
1
eleq2i
⊢ x ∈ A ↔ x ∈ B
4
3 2
anbi12i
⊢ x ∈ A ∧ ψ ↔ x ∈ B ∧ χ
5
4
rexbii2
⊢ ∃ x ∈ A ψ ↔ ∃ x ∈ B χ