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

Theorem ceqsexv2d 3518
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 3515 . . 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 394   = wceq 1533  wex 1773  wcel 2098  Vcvv 3463
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 395  df-ex 1774  df-clel 2802
This theorem is referenced by:  en0  9036  en0OLD  9037  en0r  9039  ensn1  9040  ensn1OLD  9041  0domg  9123  tz9.1  9752  cplem2  9913  karden  9918  pwmnd  18893  2lgslem1  27345  griedg0prc  29121  1loopgrvd2  29361  bnj150  34564  fnchoice  44456  nfermltl8rev  47145  nfermltl2rev  47146  nfermltlrev  47147  nn0mnd  47353  rrx2xpreen  47904
  Copyright terms: Public domain W3C validator