Theorem ceqsexv2d 3486

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ∃wex 1780   ∈ wcel 2110  Vcvv 3434

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2804

This theorem is referenced by:  en0  8935  en0r  8937  ensn1  8938  0domg  9012  tz9.1  9614  cplem2  9775  karden  9780  pwmnd  18837  2lgslem1  27325  griedg0prc  29235  1loopgrvd2  29475  bnj150  34878  permaxsep  45019  permaxnul  45020  permaxpow  45021  permaxpr  45022  permaxun  45023  permaxinf2lem  45024  nregmodel  45029  fnchoice  45045  nfermltl8rev  47752  nfermltl2rev  47753  nfermltlrev  47754  gpg5edgnedg  48140  nn0mnd  48189  rrx2xpreen  48730