Theorem ceqsexv2d 3503

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569  ∃wex 1808   ∈ wcel 2142  Vcvv 3454

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-clel 2837

This theorem is used by:  en0  9013  en0r  9015  ensn1  9016  0domg  9090  tz9.1  9696  cplem2  9879  cplem2OLD  9880  karden  9886  kardenOLD  9887  pwmnd  19005  2lgslem1  27569  griedg0prc  29625  1loopgrvd2  29864  bnj150  35273  permaxsep  45744  permaxnul  45745  permaxpow  45746  permaxpr  45747  permaxun  45748  permaxinf2lem  45749  nregmodel  45754  fnchoice  45777  nfermltl8rev  48535  nfermltl2rev  48536  nfermltlrev  48537  gpg5edgnedg  48923  nn0mnd  48972  rrx2xpreen  49527