Theorem ral0 4414

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

Syntax hints:   ∈ wcel 2111  ∀wral 3106  ∅c0 4243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-dif 3884  df-nul 4244

This theorem is referenced by:  int0  4852  0iin  4950  po0  5454  so0  5473  mpt0  6462  ixp0x  8473  ac6sfi  8746  sup0riota  8913  infpssrlem4  9717  axdc3lem4  9864  0tsk  10166  uzsupss  12328  xrsupsslem  12688  xrinfmsslem  12689  xrsup0  12704  fsuppmapnn0fiubex  13355  swrd0  14011  swrdspsleq  14018  repswsymballbi  14133  cshw1  14175  rexfiuz  14699  lcmf0  15968  2prm  16026  0ssc  17099  0subcat  17100  drsdirfi  17540  0pos  17556  mrelatglb0  17787  sgrp0b  17901  ga0  18420  psgnunilem3  18616  lbsexg  19929  ocv0  20366  mdetunilem9  21225  imasdsf1olem  22980  prdsxmslem2  23136  lebnumlem3  23568  cniccbdd  24065  ovolicc2lem4  24124  c1lip1  24600  ulm0  24986  istrkg2ld  26254  nbgr0vtx  27146  nbgr1vtx  27148  cplgr0  27215  cplgr1v  27220  wwlksn0s  27647  clwwlkn  27811  clwwlkn1  27826  0ewlk  27899  1ewlk  27900  0wlk  27901  0conngr  27977  frgr0v  28047  frgr0  28050  frgr1v  28056  1vwmgr  28061  chocnul  29111  locfinref  31194  esumnul  31417  derang0  32529  unt0  33050  nulsslt  33375  nulssgt  33376  fdc  35183  lub0N  36485  glb0N  36489  0psubN  37045  iso0  41011  fnchoice  41658  eliuniincex  41745  eliincex  41746  limcdm0  42260  2ffzoeq  43885  iccpartiltu  43939  iccpartigtl  43940  0mgm  44394  linds0  44874