Theorem ral0 4444

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

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

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

Syntax hints:   = wceq 1539  ∀wral 3065  ∅c0 4257

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-ral 3070  df-dif 3891  df-nul 4258

This theorem is referenced by:  int0  4894  0iin  4994  po0  5521  so0  5540  mpt0  6584  ixp0x  8723  ac6sfi  9067  sup0riota  9233  infpssrlem4  10071  axdc3lem4  10218  0tsk  10520  uzsupss  12689  xrsupsslem  13050  xrinfmsslem  13051  xrsup0  13066  fsuppmapnn0fiubex  13721  swrd0  14380  swrdspsleq  14387  repswsymballbi  14502  cshw1  14544  rexfiuz  15068  lcmf0  16348  2prm  16406  0ssc  17561  0subcat  17562  drsdirfi  18032  0pos  18048  0posOLD  18049  mrelatglb0  18288  sgrp0b  18392  ga0  18913  psgnunilem3  19113  lbsexg  20435  ocv0  20891  mdetunilem9  21778  imasdsf1olem  23535  prdsxmslem2  23694  lebnumlem3  24135  cniccbdd  24634  ovolicc2lem4  24693  c1lip1  25170  ulm0  25559  istrkg2ld  26830  nbgr0vtx  27732  nbgr1vtx  27734  cplgr0  27801  cplgr1v  27806  wwlksn0s  28235  clwwlkn  28399  clwwlkn1  28414  0ewlk  28487  1ewlk  28488  0wlk  28489  0conngr  28565  frgr0v  28635  frgr0  28638  frgr1v  28644  1vwmgr  28649  chocnul  29699  locfinref  31800  esumnul  32025  derang0  33140  unt0  33661  naddid1  33845  fdc  35912  lub0N  37210  glb0N  37214  0psubN  37770  sticksstones11  40119  iso0  41932  fnchoice  42579  eliuniincex  42666  eliincex  42667  limcdm0  43166  2ffzoeq  44831  iccpartiltu  44885  iccpartigtl  44886  0mgm  45339  linds0  45817  0thincg  46342