Theorem ral0 4456

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

Syntax hints:   ∈ wcel 2114  ∀wral 3138  ∅c0 4291

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 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-ral 3143  df-dif 3939  df-nul 4292

This theorem is referenced by:  int0  4890  0iin  4987  po0  5490  so0  5509  mpt0  6490  ixp0x  8490  ac6sfi  8762  sup0riota  8929  infpssrlem4  9728  axdc3lem4  9875  0tsk  10177  uzsupss  12341  xrsupsslem  12701  xrinfmsslem  12702  xrsup0  12717  fsuppmapnn0fiubex  13361  swrd0  14020  swrdspsleq  14027  repswsymballbi  14142  cshw1  14184  rexfiuz  14707  lcmf0  15978  2prm  16036  0ssc  17107  0subcat  17108  drsdirfi  17548  0pos  17564  mrelatglb0  17795  sgrp0b  17909  ga0  18428  psgnunilem3  18624  lbsexg  19936  ocv0  20821  mdetunilem9  21229  imasdsf1olem  22983  prdsxmslem2  23139  lebnumlem3  23567  cniccbdd  24062  ovolicc2lem4  24121  c1lip1  24594  ulm0  24979  istrkg2ld  26246  nbgr0vtx  27138  nbgr1vtx  27140  cplgr0  27207  cplgr1v  27212  wwlksn0s  27639  clwwlkn  27804  clwwlkn1  27819  0ewlk  27893  1ewlk  27894  0wlk  27895  0conngr  27971  frgr0v  28041  frgr0  28044  frgr1v  28050  1vwmgr  28055  chocnul  29105  locfinref  31105  esumnul  31307  derang0  32416  unt0  32937  nulsslt  33262  nulssgt  33263  fdc  35035  lub0N  36340  glb0N  36344  0psubN  36900  iso0  40659  fnchoice  41306  eliuniincex  41395  eliincex  41396  limcdm0  41919  2ffzoeq  43548  iccpartiltu  43602  iccpartigtl  43603  0mgm  44061  linds0  44540