Theorem ceqsexv2d 3502

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1568  ∃wex 1807   ∈ wcel 2141  Vcvv 3453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-clel 2836

This theorem is referenced by:  en0  9014  en0r  9016  ensn1  9017  0domg  9091  tz9.1  9697  cplem2  9875  karden  9880  pwmnd  18998  2lgslem1  27534  griedg0prc  29580  1loopgrvd2  29819  bnj150  35230  permaxsep  45686  permaxnul  45687  permaxpow  45688  permaxpr  45689  permaxun  45690  permaxinf2lem  45691  nregmodel  45696  fnchoice  45719  nfermltl8rev  48474  nfermltl2rev  48475  nfermltlrev  48476  gpg5edgnedg  48862  nn0mnd  48911  rrx2xpreen  49466