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

Theorem ral0 4028
Description: Vacuous universal quantification is always true. (Contributed by NM, 20-Oct-2005.)
Assertion
Ref Expression
ral0 𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0
StepHypRef Expression
1 noel 3878 . . 3 ¬ 𝑥 ∈ ∅
21pm2.21i 115 . 2 (𝑥 ∈ ∅ → 𝜑)
32rgen 2906 1 𝑥 ∈ ∅ 𝜑
Colors of variables: wff setvar class
Syntax hints:  wcel 1977  wral 2896  c0 3874
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-v 3175  df-dif 3543  df-nul 3875
This theorem is referenced by:  int0  4425  0iin  4514  po0  4974  so0  4992  mpt0  5934  ixp0x  7822  ac6sfi  8089  sup0riota  8254  infpssrlem4  9011  axdc3lem4  9158  0tsk  9456  uzsupss  11656  xrsupsslem  12009  xrinfmsslem  12010  xrsup0  12025  fsuppmapnn0fiubex  12654  swrd0  13286  swrdspsleq  13301  repswsymballbi  13378  cshw1  13419  rexfiuz  13935  lcmf0  15185  2prm  15243  0ssc  16320  0subcat  16321  drsdirfi  16761  0pos  16777  mrelatglb0  17008  mgm0  17078  sgrp0  17114  sgrp0b  17115  ga0  17554  psgnunilem3  17739  lbsexg  18985  ocv0  19840  mdetunilem9  20245  imasdsf1olem  21988  prdsxmslem2  22144  lebnumlem3  22570  cniccbdd  23037  ovolicc2lem4  23095  c1lip1  23564  ulm0  23949  istrkg2ld  25159  cusgra0v  25989  cusgra1v  25990  uvtx0  26019  0wlk  26075  0trl  26076  0conngra  26202  wwlkn0s  26233  0vgrargra  26464  eupa0  26501  frgra0v  26520  frgra1v  26525  1vwmgra  26530  chocnul  27571  locfinref  29236  esumnul  29437  derang0  30405  unt0  30842  nofulllem1  31101  fdc  32711  lub0N  33494  glb0N  33498  0psubN  34053  iso0  37528  fnchoice  38211  eliuniincex  38323  eliincex  38324  limcdm0  38685  iccpartiltu  39960  iccpartigtl  39961  2ffzoeq  40361  nbgr0vtx  40578  nbgr1vtx  40580  uvtxa01vtx0  40623  cplgr0  40647  cplgr0v  40649  cplgr1v  40652  wwlksn0s  41057  0ewlk  41282  1ewlk  41283  01wlk  41284  0conngr  41359  0vconngr  41360  frgr0v  41433  frgr0  41436  frgr1v  41441  1vwmgr  41446  0mgm  41564  linds0  42048
  Copyright terms: Public domain W3C validator