Theorem ceqsexv2d 3502

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 3471	. 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 2145  Vcvv 3453

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 1943  ax-6 2000  ax-7 2041  ax-8 2147

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

This theorem is used by:  en0  9027  en0r  9029  ensn1  9030  0domg  9105  tz9.1  9711  cplem2  9894  cplem2OLD  9895  karden  9901  kardenOLD  9902  degenmgm2nfun  19053  pwmnd  19057  2lgslem1  27628  griedg0prc  29710  1loopgrvd2  29949  bnj150  35372  permaxsep  45817  permaxnul  45818  permaxpow  45819  permaxpr  45820  permaxun  45821  permaxinf2lem  45822  nregmodel  45827  fnchoice  45850  nfermltl8rev  48645  nfermltl2rev  48646  nfermltlrev  48647  gpg5edgnedg  49033  nn0mnd  49081  rrx2xpreen  49636