Theorem ral0 4479

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

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

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

Syntax hints:   = wceq 1540  ∀wral 3045  ∅c0 4299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-ral 3046  df-dif 3920  df-nul 4300

This theorem is referenced by:  int0  4929  0iin  5031  po0  5566  so0  5587  mpt0  6663  naddrid  8650  ixp0x  8902  ac6sfi  9238  sup0riota  9424  infpssrlem4  10266  axdc3lem4  10413  0tsk  10715  uzsupss  12906  xrsupsslem  13274  xrinfmsslem  13275  xrsup0  13290  fsuppmapnn0fiubex  13964  swrd0  14630  swrdspsleq  14637  repswsymballbi  14752  cshw1  14794  rexfiuz  15321  lcmf0  16611  2prm  16669  0ssc  17806  0subcat  17807  drsdirfi  18273  0pos  18289  mrelatglb0  18527  sgrp0b  18662  ga0  19237  psgnunilem3  19433  lbsexg  21081  ocv0  21593  mdetunilem9  22514  imasdsf1olem  24268  prdsxmslem2  24424  lebnumlem3  24869  cniccbdd  25369  ovolicc2lem4  25428  c1lip1  25909  ulm0  26307  precsexlem9  28124  n0sfincut  28253  zscut  28302  twocut  28316  addhalfcut  28341  istrkg2ld  28394  nbgr1vtx  29292  cplgr0  29359  cplgr1v  29364  wwlksn0s  29798  clwwlkn  29962  clwwlkn1  29977  0ewlk  30050  1ewlk  30051  0wlk  30052  0conngr  30128  frgr0v  30198  frgr0  30201  frgr1v  30207  1vwmgr  30212  chocnul  31264  s1chn  32943  chnub  32945  locfinref  33838  esumnul  34045  derang0  35163  unt0  35705  fdc  37746  lub0N  39189  glb0N  39193  0psubN  39750  sticksstones11  42151  cantnfresb  43320  safesnsupfilb  43414  nla0002  43420  nla0003  43421  iso0  44303  fnchoice  45030  eliuniincex  45110  eliincex  45111  limcdm0  45623  2ffzoeq  47332  iccpartiltu  47427  iccpartigtl  47428  0mgm  48158  linds0  48458  0funcALT  49081  0thincg  49451  termolmd  49663