Theorem ceqsexv2d 3504

Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by Thierry Arnoux, 10-Sep-2016.) Shorten, reduce dv conditions. (Revised by Wolf Lammen, 5-Jun-2025.) (Proof shortened by SN, 5-Jun-2025.)

Hypotheses

Ref	Expression
ceqsexv2d.1	⊢ 𝐴 ∈ V
ceqsexv2d.2	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
ceqsexv2d.3	⊢ 𝜓

Assertion

Ref	Expression
ceqsexv2d	⊢ ∃𝑥𝜑

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem ceqsexv2d

Step	Hyp	Ref	Expression
1		ceqsexv2d.1	. . 3 ⊢ 𝐴 ∈ V
2	1	isseti 3473	. 2 ⊢ ∃𝑥 𝑥 = 𝐴
3		ceqsexv2d.3	. . 3 ⊢ 𝜓
4		ceqsexv2d.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
5	3, 4	mpbiri 260	. 2 ⊢ (𝑥 = 𝐴 → 𝜑)
6	2, 5	eximii 1858	1 ⊢ ∃𝑥𝜑

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1561  ∃wex 1800   ∈ wcel 2143  Vcvv 3455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1801  df-clel 2838

This theorem is referenced by:  en0  8999  en0r  9001  ensn1  9002  0domg  9076  tz9.1  9682  cplem2  9860  karden  9865  pwmnd  18984  2lgslem1  27465  griedg0prc  29472  1loopgrvd2  29711  bnj150  35173  permaxsep  45574  permaxnul  45575  permaxpow  45576  permaxpr  45577  permaxun  45578  permaxinf2lem  45579  nregmodel  45584  fnchoice  45600  nfermltl8rev  48355  nfermltl2rev  48356  nfermltlrev  48357  gpg5edgnedg  48743  nn0mnd  48792  rrx2xpreen  49332