Theorem ral0 4438

Description: Vacuous universal quantification is always true. (Contributed by NM, 20-Oct-2005.) Avoid df-clel 2811, ax-8 2116. (Revised by GG, 2-Sep-2024.)

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

Step	Hyp	Ref	Expression
1		eqid 2736	. 2 ⊢ ∅ = ∅
2		rzal 4434	. 2 ⊢ (∅ = ∅ → ∀𝑥 ∈ ∅ 𝜑)
3	1, 2	ax-mp 5	1 ⊢ ∀𝑥 ∈ ∅ 𝜑

Syntax hints:   = wceq 1542  ∀wral 3051  ∅c0 4273

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-ral 3052  df-dif 3892  df-nul 4274

This theorem is referenced by:  int0  4904  0iin  5006  po0  5556  so0  5577  mpt0  6640  naddrid  8619  ixp0x  8874  ac6sfi  9194  sup0riota  9379  infpssrlem4  10228  axdc3lem4  10375  0tsk  10678  uzsupss  12890  xrsupsslem  13259  xrinfmsslem  13260  xrsup0  13275  fsuppmapnn0fiubex  13954  swrd0  14621  swrdspsleq  14628  repswsymballbi  14742  cshw1  14784  rexfiuz  15310  lcmf0  16603  2prm  16661  0ssc  17804  0subcat  17805  drsdirfi  18271  0pos  18287  mrelatglb0  18527  s1chn  18586  chnub  18588  sgrp0b  18696  ga0  19273  psgnunilem3  19471  lbsexg  21162  ocv0  21657  mdetunilem9  22585  imasdsf1olem  24338  prdsxmslem2  24494  lebnumlem3  24930  cniccbdd  25428  ovolicc2lem4  25487  c1lip1  25964  ulm0  26356  rightge0  27813  precsexlem9  28207  onsbnd  28273  n0fincut  28347  zcuts  28399  twocut  28415  addhalfcut  28451  0reno  28488  istrkg2ld  28528  nbgr1vtx  29427  cplgr0  29494  cplgr1v  29499  wwlksn0s  29929  clwwlkn  30096  clwwlkn1  30111  0ewlk  30184  1ewlk  30185  0wlk  30186  0conngr  30262  frgr0v  30332  frgr0  30335  frgr1v  30341  1vwmgr  30346  chocnul  31399  locfinref  33985  esumnul  34192  derang0  35351  unt0  35893  fdc  38066  lub0N  39635  glb0N  39639  0psubN  40195  sticksstones11  42595  cantnfresb  43752  safesnsupfilb  43845  nla0002  43851  nla0003  43852  iso0  44734  fnchoice  45460  eliuniincex  45539  eliincex  45540  limcdm0  46048  2ffzoeq  47776  iccpartiltu  47882  iccpartigtl  47883  0mgm  48642  linds0  48941  0funcALT  49563  0thincg  49933  termolmd  50145