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

Theorem ral0 4271
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 4120 . . 3 ¬ 𝑥 ∈ ∅
21pm2.21i 117 . 2 (𝑥 ∈ ∅ → 𝜑)
32rgen 3110 1 𝑥 ∈ ∅ 𝜑
Colors of variables: wff setvar class
Syntax hints:  wcel 2156  wral 3096  c0 4116
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-v 3393  df-dif 3772  df-nul 4117
This theorem is referenced by:  int0  4683  0iin  4770  po0  5247  so0  5265  mpt0  6232  ixp0x  8173  ac6sfi  8443  sup0riota  8610  infpssrlem4  9413  axdc3lem4  9560  0tsk  9862  uzsupss  11999  xrsupsslem  12355  xrinfmsslem  12356  xrsup0  12371  fsuppmapnn0fiubex  13015  swrd0  13658  swrdspsleq  13673  repswsymballbi  13751  cshw1  13792  rexfiuz  14310  lcmf0  15566  2prm  15623  0ssc  16701  0subcat  16702  drsdirfi  17143  0pos  17159  mrelatglb0  17390  sgrp0b  17497  ga0  17932  psgnunilem3  18117  lbsexg  19373  ocv0  20231  mdetunilem9  20637  imasdsf1olem  22391  prdsxmslem2  22547  lebnumlem3  22975  cniccbdd  23442  ovolicc2lem4  23501  c1lip1  23974  ulm0  24359  istrkg2ld  25573  nbgr0vtx  26468  nbgr1vtx  26470  uvtxa01vtx0OLD  26520  prcliscplgr  26537  cplgr0  26549  cplgr1v  26554  wwlksn0s  26988  clwwlkn  27171  clwwlkn1  27190  0ewlk  27287  1ewlk  27288  0wlk  27289  0conngr  27365  frgr0v  27436  frgr0  27439  frgr1v  27446  1vwmgr  27451  chocnul  28515  locfinref  30233  esumnul  30435  derang0  31474  unt0  31910  nulsslt  32229  nulssgt  32230  fdc  33852  lub0N  34969  glb0N  34973  0psubN  35529  iso0  39006  fnchoice  39682  eliuniincex  39784  eliincex  39785  limcdm0  40330  2ffzoeq  41913  iccpartiltu  41933  iccpartigtl  41934  0mgm  42342  linds0  42822
  Copyright terms: Public domain W3C validator