Theorem ceqsexv2d 3496

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 3462	. 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 2109  Vcvv 3444

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 2008  ax-8 2111

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

This theorem is referenced by:  en0  8966  en0r  8968  ensn1  8969  0domg  9045  tz9.1  9658  cplem2  9819  karden  9824  pwmnd  18846  2lgslem1  27338  griedg0prc  29244  1loopgrvd2  29484  bnj150  34859  permaxsep  44990  permaxnul  44991  permaxpow  44992  permaxpr  44993  permaxun  44994  permaxinf2lem  44995  nregmodel  45000  fnchoice  45016  nfermltl8rev  47736  nfermltl2rev  47737  nfermltlrev  47738  nn0mnd  48160  rrx2xpreen  48701