Theorem ceqsexv2d 3498

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 3495	. . 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 3446

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 2809

This theorem is referenced by:  en0  8964  en0OLD  8965  en0r  8967  ensn1  8968  ensn1OLD  8969  0domg  9051  tz9.1  9674  cplem2  9835  karden  9840  pwmnd  18761  2lgslem1  26779  griedg0prc  28275  1loopgrvd2  28514  bnj150  33577  fnchoice  43356  nfermltl8rev  46054  nfermltl2rev  46055  nfermltlrev  46056  nn0mnd  46233  rrx2xpreen  46925