Theorem ceqsexv2d 3499

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569  ∃wex 1811   ∈ wcel 2144  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-clel 2835

This theorem is used by:  en0  9045  en0r  9047  ensn1  9048  0domg  9123  tz9.1  9730  cplem2  9952  cplem2OLD  9953  karden  9959  kardenOLD  9960  degenmgm2nfun  19139  pwmnd  19143  2lgslem1  27721  griedg0prc  29845  1loopgrvd2  30084  bnj150  35548  permaxsep  46040  permaxnul  46041  permaxpow  46042  permaxpr  46043  permaxun  46044  permaxinf2lem  46045  nregmodel  46050  fnchoice  46089  nfermltl8rev  48883  nfermltl2rev  48884  nfermltlrev  48885  gpg5edgnedg  49271  nn0mnd  49319  rrx2xpreen  49874