Theorem ral0 4458

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 4298	. . 3 ⊢ ¬ 𝑥 ∈ ∅
2	1	pm2.21i 119	. 2 ⊢ (𝑥 ∈ ∅ → 𝜑)
3	2	rgen 3150	1 ⊢ ∀𝑥 ∈ ∅ 𝜑

Syntax hints:   ∈ wcel 2114  ∀wral 3140  ∅c0 4293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-ral 3145  df-dif 3941  df-nul 4294

This theorem is referenced by:  int0  4892  0iin  4989  po0  5492  so0  5511  mpt0  6492  ixp0x  8492  ac6sfi  8764  sup0riota  8931  infpssrlem4  9730  axdc3lem4  9877  0tsk  10179  uzsupss  12343  xrsupsslem  12703  xrinfmsslem  12704  xrsup0  12719  fsuppmapnn0fiubex  13363  swrd0  14022  swrdspsleq  14029  repswsymballbi  14144  cshw1  14186  rexfiuz  14709  lcmf0  15980  2prm  16038  0ssc  17109  0subcat  17110  drsdirfi  17550  0pos  17566  mrelatglb0  17797  sgrp0b  17911  ga0  18430  psgnunilem3  18626  lbsexg  19938  ocv0  20823  mdetunilem9  21231  imasdsf1olem  22985  prdsxmslem2  23141  lebnumlem3  23569  cniccbdd  24064  ovolicc2lem4  24123  c1lip1  24596  ulm0  24981  istrkg2ld  26248  nbgr0vtx  27140  nbgr1vtx  27142  cplgr0  27209  cplgr1v  27214  wwlksn0s  27641  clwwlkn  27806  clwwlkn1  27821  0ewlk  27895  1ewlk  27896  0wlk  27897  0conngr  27973  frgr0v  28043  frgr0  28046  frgr1v  28052  1vwmgr  28057  chocnul  29107  locfinref  31107  esumnul  31309  derang0  32418  unt0  32939  nulsslt  33264  nulssgt  33265  fdc  35022  lub0N  36327  glb0N  36331  0psubN  36887  iso0  40646  fnchoice  41293  eliuniincex  41382  eliincex  41383  limcdm0  41906  2ffzoeq  43535  iccpartiltu  43589  iccpartigtl  43590  0mgm  44048  linds0  44527