Theorem ceqsexv2d 3487

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 3454	. 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 2111  Vcvv 3436

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 2113

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

This theorem is referenced by:  en0  8946  en0r  8948  ensn1  8949  0domg  9023  tz9.1  9625  cplem2  9789  karden  9794  pwmnd  18851  2lgslem1  27338  griedg0prc  29249  1loopgrvd2  29489  bnj150  34895  permaxsep  45105  permaxnul  45106  permaxpow  45107  permaxpr  45108  permaxun  45109  permaxinf2lem  45110  nregmodel  45115  fnchoice  45131  nfermltl8rev  47847  nfermltl2rev  47848  nfermltlrev  47849  gpg5edgnedg  48235  nn0mnd  48284  rrx2xpreen  48825