Theorem ral0 3873

Description: Vacuous universal quantification is always true. (Contributed by NM, 20-Oct-2005.)

Assertion

Ref	Expression
ral0	|- A. x e. (/) ph

Proof of Theorem ral0

Step	Hyp	Ref	Expression
1		noel 3734	. . 3 |- -. x e. (/)
2	1	pm2.21i 135	. 2 |- ( x e. (/) -> ph )
3	2	rgen 2746	1 |- A. x e. (/) ph

Syntax hints:   e. wcel 1886   A.wral 2736   (/)c0 3730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ral 2741  df-v 3046  df-dif 3406  df-nul 3731

This theorem is referenced by:  0iin  4335  po0  4769  so0  4787  mpt0  5703  ixp0x  7547  ac6sfi  7812  sup0riota  7976  infpssrlem4  8733  axdc3lem4  8880  0tsk  9177  uzsupss  11253  xrsupsslem  11589  xrinfmsslem  11590  xrsup0  11606  fsuppmapnn0fiubex  12201  swrd0  12785  swrdspsleq  12800  repswsymballbi  12878  cshw1  12916  rexfiuz  13403  lcmf0  14600  2prm  14633  0ssc  15735  0subcat  15736  drsdirfi  16176  0pos  16193  mrelatglb0  16424  ga0  16945  psgnunilem3  17130  lbsexg  18380  ocv0  19233  mdetunilem9  19638  imasdsf1olem  21381  prdsxmslem2  21537  lebnumlem3  21984  lebnumlem3OLD  21987  cniccbdd  22405  ovolicc2lem4OLD  22466  ovolicc2lem4  22467  c1lip1  22942  ulm0  23339  istrkg2ld  24501  cusgra0v  25181  cusgra1v  25182  uvtx0  25212  0wlk  25268  0trl  25269  0conngra  25395  wwlkn0s  25426  0vgrargra  25658  eupa0  25695  frgra0v  25714  frgra1v  25719  1vwmgra  25724  chocnul  26974  locfinref  28661  esumnul  28862  derang0  29885  unt0  30331  nofulllem1  30584  fdc  32067  lub0N  32749  glb0N  32753  0psubN  33308  iso0  36649  fnchoice  37344  limcdm0  37692  iccpartiltu  38730  iccpartigtl  38731  2ffzoeq  39051  nbgr0vtx  39407  nbgr1vtx  39409  uvtxa01vtx0  39452  cplgr0  39476  cplgr0v  39478  cplgr1v  39480  0ewlk  39605  1ewlk  39607  01wlk  39647  0mgm  39761  linds0  40245