Theorem ceqsexv2d 3528

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 3525	. . 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 1541  ∃wex 1781   ∈ wcel 2106  Vcvv 3474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  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 1782  df-clel 2810

This theorem is referenced by:  en0  9015  en0OLD  9016  en0r  9018  ensn1  9019  ensn1OLD  9020  0domg  9102  tz9.1  9726  cplem2  9887  karden  9892  pwmnd  18820  2lgslem1  26904  griedg0prc  28559  1loopgrvd2  28798  bnj150  33956  fnchoice  43795  nfermltl8rev  46489  nfermltl2rev  46490  nfermltlrev  46491  nn0mnd  46668  rrx2xpreen  47483