Theorem ceqsexv2d 3493

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 260	. 2 ⊢ (𝑥 = 𝐴 → 𝜑)
6	2, 5	eximii 1847	1 ⊢ ∃𝑥𝜑

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1550  ∃wex 1789   ∈ wcel 2132  Vcvv 3444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1790  df-clel 2827

This theorem is referenced by:  en0  8984  en0r  8986  ensn1  8987  0domg  9061  tz9.1  9670  cplem2  9834  karden  9839  pwmnd  18946  2lgslem1  27424  griedg0prc  29400  1loopgrvd2  29639  bnj150  35118  permaxsep  45521  permaxnul  45522  permaxpow  45523  permaxpr  45524  permaxun  45525  permaxinf2lem  45526  nregmodel  45531  fnchoice  45547  nfermltl8rev  48302  nfermltl2rev  48303  nfermltlrev  48304  gpg5edgnedg  48690  nn0mnd  48739  rrx2xpreen  49279