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
⊢ ( 𝜑 → 𝐴 = 𝐵 )
raleqbidvv.2
⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
Assertion
rexeqbidvv
⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜓 ↔ ∃ 𝑥 ∈ 𝐵 𝜒 ) )
Proof
Step
Hyp
Ref
Expression
1
raleqbidvv.1
⊢ ( 𝜑 → 𝐴 = 𝐵 )
2
raleqbidvv.2
⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
3
2
adantr
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
4
1 3
rexeqbidva
⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜓 ↔ ∃ 𝑥 ∈ 𝐵 𝜒 ) )