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

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
StepHypRef Expression
1 ceqsexv2d.3 . 2 𝜓
2 ceqsexv2d.1 . . . 4 𝐴 ∈ V
3 ceqsexv2d.2 . . . 4 (𝑥 = 𝐴 → (𝜑𝜓))
42, 3ceqsexv 3455 . . 3 (∃𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓)
54biimpri 231 . 2 (𝜓 → ∃𝑥(𝑥 = 𝐴𝜑))
6 exsimpr 1877 . 2 (∃𝑥(𝑥 = 𝐴𝜑) → ∃𝑥𝜑)
71, 5, 6mp2b 10 1 𝑥𝜑
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator