Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
The universal class
ceqsexv2dOLD
Metamath Proof Explorer
Description: Obsolete version of ceqsexv2d as of 5-Jun-2025. (Contributed by Thierry Arnoux , 10-Sep-2016) (Proof modification is discouraged.)
(New usage is discouraged.)
Ref
Expression
Hypotheses
ceqsexv2dOLD.1
⊢ 𝐴 ∈ V
ceqsexv2dOLD.2
⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
ceqsexv2dOLD.3
⊢ 𝜓
Assertion
ceqsexv2dOLD
⊢ ∃ 𝑥 𝜑
Proof
Step
Hyp
Ref
Expression
1
ceqsexv2dOLD.1
⊢ 𝐴 ∈ V
2
ceqsexv2dOLD.2
⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
3
ceqsexv2dOLD.3
⊢ 𝜓
4
1 2
ceqsexv
⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ 𝜓 )
5
4
biimpri
⊢ ( 𝜓 → ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) )
6
exsimpr
⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) → ∃ 𝑥 𝜑 )
7
3 5 6
mp2b
⊢ ∃ 𝑥 𝜑