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

Theorem ral0 4458
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 4299 . . 3 ¬ 𝑥 ∈ ∅
21pm2.21i 119 . 2 (𝑥 ∈ ∅ → 𝜑)
32rgen 3152 1 𝑥 ∈ ∅ 𝜑
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  wral 3142  c0 4294
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-ral 3147  df-dif 3942  df-nul 4295
This theorem is referenced by:  int0  4887  0iin  4983  po0  5488  so0  5507  mpt0  6486  ixp0x  8482  ac6sfi  8754  sup0riota  8921  infpssrlem4  9720  axdc3lem4  9867  0tsk  10169  uzsupss  12332  xrsupsslem  12693  xrinfmsslem  12694  xrsup0  12709  fsuppmapnn0fiubex  13353  swrd0  14013  swrdspsleq  14020  repswsymballbi  14135  cshw1  14177  rexfiuz  14700  lcmf0  15970  2prm  16028  0ssc  17099  0subcat  17100  drsdirfi  17540  0pos  17556  mrelatglb0  17787  sgrp0b  17900  ga0  18360  psgnunilem3  18546  lbsexg  19858  ocv0  20739  mdetunilem9  21147  imasdsf1olem  22900  prdsxmslem2  23056  lebnumlem3  23484  cniccbdd  23979  ovolicc2lem4  24038  c1lip1  24511  ulm0  24896  istrkg2ld  26162  nbgr0vtx  27054  nbgr1vtx  27056  cplgr0  27123  cplgr1v  27128  wwlksn0s  27555  clwwlkn  27720  clwwlkn1  27735  0ewlk  27809  1ewlk  27810  0wlk  27811  0conngr  27887  frgr0v  27957  frgr0  27960  frgr1v  27966  1vwmgr  27971  chocnul  29021  locfinref  30993  esumnul  31195  derang0  32302  unt0  32823  nulsslt  33148  nulssgt  33149  fdc  34890  lub0N  36194  glb0N  36198  0psubN  36754  iso0  40506  fnchoice  41153  eliuniincex  41243  eliincex  41244  limcdm0  41766  2ffzoeq  43396  iccpartiltu  43416  iccpartigtl  43417  0mgm  43875  linds0  44354
  Copyright terms: Public domain W3C validator