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

Theorem ceqsexv2d 3495
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 3492 . . 3 (∃𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓)
54biimpri 227 . 2 (𝜓 → ∃𝑥(𝑥 = 𝐴𝜑))
6 exsimpr 1872 . 2 (∃𝑥(𝑥 = 𝐴𝜑) → ∃𝑥𝜑)
71, 5, 6mp2b 10 1 𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wex 1781  wcel 2106  Vcvv 3443
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 2815
This theorem is referenced by:  en0  8890  en0OLD  8891  en0r  8893  ensn1  8894  ensn1OLD  8895  0domg  8977  tz9.1  9598  cplem2  9759  karden  9764  pwmnd  18681  2lgslem1  26664  griedg0prc  28010  1loopgrvd2  28249  bnj150  33261  fnchoice  42998  nfermltl8rev  45683  nfermltl2rev  45684  nfermltlrev  45685  nn0mnd  45862  rrx2xpreen  46554
  Copyright terms: Public domain W3C validator