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

Theorem ral0 4109
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 3952 . . 3 ¬ 𝑥 ∈ ∅
21pm2.21i 116 . 2 (𝑥 ∈ ∅ → 𝜑)
32rgen 2951 1 𝑥 ∈ ∅ 𝜑
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  wral 2941  c0 3948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-v 3233  df-dif 3610  df-nul 3949
This theorem is referenced by:  int0  4522  0iin  4610  po0  5079  so0  5097  mpt0  6059  ixp0x  7978  ac6sfi  8245  sup0riota  8412  infpssrlem4  9166  axdc3lem4  9313  0tsk  9615  uzsupss  11818  xrsupsslem  12175  xrinfmsslem  12176  xrsup0  12191  fsuppmapnn0fiubex  12832  swrd0  13480  swrdspsleq  13495  repswsymballbi  13573  cshw1  13614  rexfiuz  14131  lcmf0  15394  2prm  15452  0ssc  16544  0subcat  16545  drsdirfi  16985  0pos  17001  mrelatglb0  17232  sgrp0b  17339  ga0  17777  psgnunilem3  17962  lbsexg  19212  ocv0  20069  mdetunilem9  20474  imasdsf1olem  22225  prdsxmslem2  22381  lebnumlem3  22809  cniccbdd  23276  ovolicc2lem4  23334  c1lip1  23805  ulm0  24190  istrkg2ld  25404  nbgr0vtx  26297  nbgr1vtx  26299  uvtxa01vtx0OLD  26348  prcliscplgr  26365  cplgr0  26377  cplgr1v  26382  wwlksn0s  26815  clwwlkn  26985  clwwlkn1  27004  0ewlk  27092  1ewlk  27093  0wlk  27094  0conngr  27170  frgr0v  27241  frgr0  27244  frgr1v  27251  1vwmgr  27256  chocnul  28315  locfinref  30036  esumnul  30238  derang0  31277  unt0  31714  nulsslt  32033  nulssgt  32034  fdc  33671  lub0N  34794  glb0N  34798  0psubN  35353  iso0  38823  fnchoice  39502  eliuniincex  39606  eliincex  39607  limcdm0  40168  2ffzoeq  41663  iccpartiltu  41683  iccpartigtl  41684  0mgm  42099  linds0  42579
  Copyright terms: Public domain W3C validator