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 1870	1 ⊢ ∃𝑥𝜑

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

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 2835

This theorem is used by:  en0  9023  en0r  9025  ensn1  9026  0domg  9101  tz9.1  9708  cplem2  9923  cplem2OLD  9924  karden  9930  kardenOLD  9931  degenmgm2nfun  19100  pwmnd  19104  2lgslem1  27684  griedg0prc  29778  1loopgrvd2  30017  bnj150  35440  permaxsep  45934  permaxnul  45935  permaxpow  45936  permaxpr  45937  permaxun  45938  permaxinf2lem  45939  nregmodel  45944  fnchoice  45967  nfermltl8rev  48762  nfermltl2rev  48763  nfermltlrev  48764  gpg5edgnedg  49150  nn0mnd  49198  rrx2xpreen  49753