Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Restricted quantification
Restricted universal and existential quantification
rexeqbidvv
Metamath Proof Explorer
Description: Version of rexeqbidv with additional disjoint variable conditions, not
requiring ax-8 nor df-clel . (Contributed by Wolf Lammen , 25-Sep-2024)
Ref
Expression
Hypotheses
raleqbidvv.1
⊢ φ → A = B
raleqbidvv.2
⊢ φ → ψ ↔ χ
Assertion
rexeqbidvv
⊢ φ → ∃ x ∈ A ψ ↔ ∃ x ∈ B χ
Proof
Step
Hyp
Ref
Expression
1
raleqbidvv.1
⊢ φ → A = B
2
raleqbidvv.2
⊢ φ → ψ ↔ χ
3
2
adantr
⊢ φ ∧ x ∈ A → ψ ↔ χ
4
1 3
rexeqbidva
⊢ φ → ∃ x ∈ A ψ ↔ ∃ x ∈ B χ