Theorem ceqsexv2d 3512

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ∃wex 1779   ∈ wcel 2108  Vcvv 3459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2809

This theorem is referenced by:  en0  9030  en0r  9032  ensn1  9033  0domg  9112  tz9.1  9741  cplem2  9902  karden  9907  pwmnd  18913  2lgslem1  27355  griedg0prc  29189  1loopgrvd2  29429  bnj150  34853  permaxsep  44980  permaxnul  44981  permaxpow  44982  permaxpr  44983  permaxun  44984  permaxinf2lem  44985  fnchoice  45001  nfermltl8rev  47704  nfermltl2rev  47705  nfermltlrev  47706  nn0mnd  48102  rrx2xpreen  48647