Theorem ceqsexv2d 3503

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 3472	. 2 ⊢ ∃𝑥 𝑥 = 𝐴
3		ceqsexv2d.3	. . 3 ⊢ 𝜓
4		ceqsexv2d.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
5	3, 4	mpbiri 261	. 2 ⊢ (𝑥 = 𝐴 → 𝜑)
6	2, 5	eximii 1870	1 ⊢ ∃𝑥𝜑

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ∃wex 1812   ∈ wcel 2147  Vcvv 3454

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2839

This theorem is used by:  en0  9073  en0r  9075  ensn1  9076  0domg  9151  tz9.1  9757  cplem2  9979  cplem2OLD  9980  karden  9986  kardenOLD  9987  degenmgm2nfun  19168  pwmnd  19172  2lgslem1  27751  griedg0prc  29875  1loopgrvd2  30114  bnj150  35576  permaxsep  46192  permaxnul  46193  permaxpow  46194  permaxpr  46195  permaxun  46196  permaxinf2lem  46197  nregmodel  46202  fnchoice  46251  nfermltl8rev  49045  nfermltl2rev  49046  nfermltlrev  49047  gpg5edgnedg  49433  nn0mnd  49481  rrx2xpreen  50037  fuconuniq2  50990