Theorem ceqsexv2d 3545

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  ∃wex 1777   ∈ wcel 2108  Vcvv 3488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-clel 2819

This theorem is referenced by:  en0  9078  en0OLD  9079  en0r  9081  ensn1  9082  ensn1OLD  9083  0domg  9166  tz9.1  9798  cplem2  9959  karden  9964  pwmnd  18972  2lgslem1  27456  griedg0prc  29299  1loopgrvd2  29539  bnj150  34852  fnchoice  44929  nfermltl8rev  47616  nfermltl2rev  47617  nfermltlrev  47618  nn0mnd  47902  rrx2xpreen  48453