Metamath Proof Explorer


Theorem ceqsexv2dOLD

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 𝑥 𝜑