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

Theorem elabd 3671
Description: Explicit demonstration the class {𝑥𝜓} is not empty by the example 𝑋. (Contributed by RP, 12-Aug-2020.)
Hypotheses
Ref Expression
elab.xex (𝜑𝑋 ∈ V)
elab.xmaj (𝜑𝜒)
elab.xsub (𝑥 = 𝑋 → (𝜓𝜒))
Assertion
Ref Expression
elabd (𝜑 → ∃𝑥𝜓)
Distinct variable groups:   𝜒,𝑥   𝑥,𝑋
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem elabd
StepHypRef Expression
1 elab.xex . 2 (𝜑𝑋 ∈ V)
2 elab.xmaj . 2 (𝜑𝜒)
3 elab.xsub . . 3 (𝑥 = 𝑋 → (𝜓𝜒))
43spcegv 3601 . 2 (𝑋 ∈ V → (𝜒 → ∃𝑥𝜓))
51, 2, 4sylc 65 1 (𝜑 → ∃𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1530  wex 1773  wcel 2107  Vcvv 3499
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 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-cleq 2818  df-clel 2897
This theorem is referenced by:  zfrep6  7650  wfrlem15  7963  ertr  8297  f1dom2g  8519  dom3d  8543  disjenex  8667  domssex2  8669  domssex  8670  brwdom2  9029  infxpenc2lem2  9438  dfac8clem  9450  ac5num  9454  acni2  9464  acnlem  9466  finnisoeu  9531  infpss  9631  cofsmo  9683  axdc4lem  9869  ac6num  9893  axdclem2  9934  hasheqf1od  13707  fz1isolem  13812  wrd2f1tovbij  14317  fsum  15070  ntrivcvgn0  15247  fprod  15288  setsexstruct2  16515  isacs1i  16921  mreacs  16922  gsumval3lem2  18949  eltg3  21489  elptr  22100  nbusgrf1o1  27069  cusgrexg  27143  cusgrfilem3  27156  sizusglecusg  27162  wwlksnextbij  27597  eqvreltr  35712  clrellem  39850  clcnvlem  39851  prproropen  43505  isomgreqve  43825  isomushgr  43826  isomgrsym  43836  isomgrtr  43839  ushrisomgr  43841  uspgrsprfo  43858  uspgrbispr  43861
  Copyright terms: Public domain W3C validator