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
⊢ A ∈ V
ceqsexv2dOLD.2
⊢ x = A → φ ↔ ψ
ceqsexv2dOLD.3
⊢ ψ
Assertion
ceqsexv2dOLD
⊢ ∃ x φ
Proof
Step
Hyp
Ref
Expression
1
ceqsexv2dOLD.1
⊢ A ∈ V
2
ceqsexv2dOLD.2
⊢ x = A → φ ↔ ψ
3
ceqsexv2dOLD.3
⊢ ψ
4
1 2
ceqsexv
⊢ ∃ x x = A ∧ φ ↔ ψ
5
4
biimpri
⊢ ψ → ∃ x x = A ∧ φ
6
exsimpr
⊢ ∃ x x = A ∧ φ → ∃ x φ
7
3 5 6
mp2b
⊢ ∃ x φ