Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ceqsexv2d Structured version   Visualization version   GIF version

Theorem ceqsexv2d 3491
 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
StepHypRef Expression
1 ceqsexv2d.3 . 2 𝜓
2 ceqsexv2d.1 . . . 4 𝐴 ∈ V
3 ceqsexv2d.2 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
42, 3ceqsexv 3490 . . 3 (∃𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓)
54biimpri 231 . 2 (𝜓 → ∃𝑥(𝑥 = 𝐴𝜑))
6 exsimpr 1870 . 2 (∃𝑥(𝑥 = 𝐴𝜑) → ∃𝑥𝜑)
71, 5, 6mp2b 10 1 𝑥𝜑
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  Vcvv 3442 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-cleq 2791  df-clel 2870 This theorem is referenced by:  ensn1  8574  tz9.1  9173  cplem2  9321  karden  9326  pwmnd  18114  2lgslem1  26022  griedg0prc  27098  1loopgrvd2  27337  bnj150  32324  fnchoice  41829  nfermltl8rev  44428  nfermltl2rev  44429  nfermltlrev  44430  nn0mnd  44607  rrx2xpreen  45299
 Copyright terms: Public domain W3C validator