Theorem ceqsexv2d 3457

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 3455	. . 3 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)
5	4	biimpri 231	. 2 ⊢ (𝜓 → ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))
6		exsimpr 1877	. 2 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) → ∃𝑥𝜑)
7	1, 5, 6	mp2b 10	1 ⊢ ∃𝑥𝜑

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543  ∃wex 1787   ∈ wcel 2110  Vcvv 3408

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-clel 2816

This theorem is referenced by:  en0  8691  en0OLD  8692  ensn1  8694  ensn1OLD  8695  tz9.1  9345  cplem2  9506  karden  9511  pwmnd  18364  2lgslem1  26275  griedg0prc  27352  1loopgrvd2  27591  bnj150  32569  fnchoice  42245  nfermltl8rev  44867  nfermltl2rev  44868  nfermltlrev  44869  nn0mnd  45046  rrx2xpreen  45738