Theorem ceqsexv2d 3458

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1539  ∃wex 1782   ∈ wcel 2112  Vcvv 3407

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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-12 2176  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-nf 1787  df-cleq 2751  df-clel 2831

This theorem is referenced by:  en0  8583  ensn1  8585  tz9.1  9189  cplem2  9337  karden  9342  pwmnd  18153  2lgslem1  26062  griedg0prc  27138  1loopgrvd2  27377  bnj150  32361  fnchoice  42016  nfermltl8rev  44612  nfermltl2rev  44613  nfermltlrev  44614  nn0mnd  44791  rrx2xpreen  45483