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

Theorem ceqsexv2d 3523
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 3520 . . 3 (∃𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓)
54biimpri 227 . 2 (𝜓 → ∃𝑥(𝑥 = 𝐴𝜑))
6 exsimpr 1864 . 2 (∃𝑥(𝑥 = 𝐴𝜑) → ∃𝑥𝜑)
71, 5, 6mp2b 10 1 𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395   = wceq 1533  wex 1773  wcel 2098  Vcvv 3468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100
This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-clel 2804
This theorem is referenced by:  en0  9015  en0OLD  9016  en0r  9018  ensn1  9019  ensn1OLD  9020  0domg  9102  tz9.1  9726  cplem2  9887  karden  9892  pwmnd  18862  2lgslem1  27282  griedg0prc  29029  1loopgrvd2  29269  bnj150  34416  fnchoice  44289  nfermltl8rev  46982  nfermltl2rev  46983  nfermltlrev  46984  nn0mnd  47129  rrx2xpreen  47680
  Copyright terms: Public domain W3C validator