Theorem ral0 4472

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

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

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

Syntax hints:   = wceq 1540  ∀wral 3044  ∅c0 4292

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 2701

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 2708  df-cleq 2721  df-ral 3045  df-dif 3914  df-nul 4293

This theorem is referenced by:  int0  4922  0iin  5023  po0  5556  so0  5577  mpt0  6642  naddrid  8624  ixp0x  8876  ac6sfi  9207  sup0riota  9393  infpssrlem4  10235  axdc3lem4  10382  0tsk  10684  uzsupss  12875  xrsupsslem  13243  xrinfmsslem  13244  xrsup0  13259  fsuppmapnn0fiubex  13933  swrd0  14599  swrdspsleq  14606  repswsymballbi  14721  cshw1  14763  rexfiuz  15290  lcmf0  16580  2prm  16638  0ssc  17775  0subcat  17776  drsdirfi  18242  0pos  18258  mrelatglb0  18496  sgrp0b  18631  ga0  19206  psgnunilem3  19402  lbsexg  21050  ocv0  21562  mdetunilem9  22483  imasdsf1olem  24237  prdsxmslem2  24393  lebnumlem3  24838  cniccbdd  25338  ovolicc2lem4  25397  c1lip1  25878  ulm0  26276  precsexlem9  28093  n0sfincut  28222  zscut  28271  twocut  28285  addhalfcut  28310  istrkg2ld  28363  nbgr1vtx  29261  cplgr0  29328  cplgr1v  29333  wwlksn0s  29764  clwwlkn  29928  clwwlkn1  29943  0ewlk  30016  1ewlk  30017  0wlk  30018  0conngr  30094  frgr0v  30164  frgr0  30167  frgr1v  30173  1vwmgr  30178  chocnul  31230  s1chn  32909  chnub  32911  locfinref  33804  esumnul  34011  derang0  35129  unt0  35671  fdc  37712  lub0N  39155  glb0N  39159  0psubN  39716  sticksstones11  42117  cantnfresb  43286  safesnsupfilb  43380  nla0002  43386  nla0003  43387  iso0  44269  fnchoice  44996  eliuniincex  45076  eliincex  45077  limcdm0  45589  2ffzoeq  47301  iccpartiltu  47396  iccpartigtl  47397  0mgm  48127  linds0  48427  0funcALT  49050  0thincg  49420  termolmd  49632