Theorem ceqsexv2d 3481

Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by Thierry Arnoux, 10-Sep-2016.)

Hypotheses

Ref	Expression
ceqsexv2d.1	⊢ 𝐴 ∈ V
ceqsexv2d.2	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
ceqsexv2d.3	⊢ 𝜓

Assertion

Ref	Expression
ceqsexv2d	⊢ ∃𝑥𝜑

Distinct variable groups:   𝑥,𝐴   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ceqsexv2d

Step	Hyp	Ref	Expression
1		ceqsexv2d.3	. 2 ⊢ 𝜓
2		ceqsexv2d.1	. . . 4 ⊢ 𝐴 ∈ V
3		ceqsexv2d.2	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	2, 3	ceqsexv 3479	. . 3 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)
5	4	biimpri 227	. 2 ⊢ (𝜓 → ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))
6		exsimpr 1872	. 2 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) → ∃𝑥𝜑)
7	1, 5, 6	mp2b 10	1 ⊢ ∃𝑥𝜑

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539  ∃wex 1782   ∈ wcel 2106  Vcvv 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-clel 2816

This theorem is referenced by:  en0  8803  en0OLD  8804  en0r  8806  ensn1  8807  ensn1OLD  8808  0domg  8887  tz9.1  9487  cplem2  9648  karden  9653  pwmnd  18576  2lgslem1  26542  griedg0prc  27631  1loopgrvd2  27870  bnj150  32856  fnchoice  42572  nfermltl8rev  45194  nfermltl2rev  45195  nfermltlrev  45196  nn0mnd  45373  rrx2xpreen  46065