Theorem ral0 4488

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

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

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

Syntax hints:   = wceq 1540  ∀wral 3051  ∅c0 4308

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 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-ral 3052  df-dif 3929  df-nul 4309

This theorem is referenced by:  int0  4938  0iin  5040  po0  5578  so0  5599  mpt0  6680  naddrid  8695  ixp0x  8940  ac6sfi  9292  sup0riota  9478  infpssrlem4  10320  axdc3lem4  10467  0tsk  10769  uzsupss  12956  xrsupsslem  13323  xrinfmsslem  13324  xrsup0  13339  fsuppmapnn0fiubex  14010  swrd0  14676  swrdspsleq  14683  repswsymballbi  14798  cshw1  14840  rexfiuz  15366  lcmf0  16653  2prm  16711  0ssc  17850  0subcat  17851  drsdirfi  18317  0pos  18333  mrelatglb0  18571  sgrp0b  18706  ga0  19281  psgnunilem3  19477  lbsexg  21125  ocv0  21637  mdetunilem9  22558  imasdsf1olem  24312  prdsxmslem2  24468  lebnumlem3  24913  cniccbdd  25414  ovolicc2lem4  25473  c1lip1  25954  ulm0  26352  precsexlem9  28169  n0sfincut  28298  zscut  28347  twocut  28361  addhalfcut  28386  istrkg2ld  28439  nbgr1vtx  29337  cplgr0  29404  cplgr1v  29409  wwlksn0s  29843  clwwlkn  30007  clwwlkn1  30022  0ewlk  30095  1ewlk  30096  0wlk  30097  0conngr  30173  frgr0v  30243  frgr0  30246  frgr1v  30252  1vwmgr  30257  chocnul  31309  s1chn  32990  chnub  32992  locfinref  33872  esumnul  34079  derang0  35191  unt0  35728  fdc  37769  lub0N  39207  glb0N  39211  0psubN  39768  sticksstones11  42169  cantnfresb  43348  safesnsupfilb  43442  nla0002  43448  nla0003  43449  iso0  44331  fnchoice  45053  eliuniincex  45133  eliincex  45134  limcdm0  45647  2ffzoeq  47356  iccpartiltu  47436  iccpartigtl  47437  0mgm  48141  linds0  48441  0funcALT  49053  0thincg  49344