Theorem ral0 3934

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

Assertion

Ref	Expression
ral0

Proof of Theorem ral0

Step	Hyp	Ref	Expression
1		noel 3788	. . 3
2	1	pm2.21i 131	. 2
3	2	rgen 2817	1

Syntax hints:  e.wcel 1818  A.wral 2807  c0 3784

This theorem is referenced by:  0iin  4388  reusv6OLD  4663  reusv7OLD  4664  po0  4820  so0  4838  mpt0  5713  ixp0x  7517  ac6sfi  7784  infpssrlem4  8707  axdc3lem4  8854  0tsk  9154  uzsupss  11203  xrsupsslem  11527  xrinfmsslem  11528  xrsup0  11544  fsuppmapnn0fiubex  12098  swrdspsleq  12673  repswsymballbi  12752  cshw1  12790  rexfiuz  13180  2prm  14233  0ssc  15206  0subcat  15207  drsdirfi  15567  0pos  15584  mrelatglb0  15815  ga0  16336  psgnunilem3  16521  lbsexg  17810  ocv0  18708  mdetunilem9  19122  imasdsf1olem  20876  prdsxmslem2  21032  lebnumlem3  21463  cniccbdd  21873  ovolicc2lem4  21931  c1lip1  22398  ulm0  22786  istrkg2ld  23858  cusgra0v  24460  cusgra1v  24461  uvtx0  24491  0wlk  24547  0trl  24548  0conngra  24674  wwlkn0s  24705  0vgrargra  24937  eupa0  24974  frgra0v  24993  frgra1v  24998  1vwmgra  25003  chocnul  26246  locfinref  27844  esumnul  28059  derang0  28613  unt0  29083  nofulllem1  29462  fdc  30238  iso0  31187  fnchoice  31404  limcdm0  31624  2ffzoeq  32341  0mgm  32462  linds0  33066  lub0N  34914  glb0N  34918  0psubN  35473

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-v 3111  df-dif 3478  df-nul 3785