Theorem ral0 4452

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

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

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

Syntax hints:   = wceq 1560  ∀wral 3076  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-ral 3077  df-dif 3907  df-nul 4286

This theorem is referenced by:  int0  4920  0iin  5021  po0  5572  so0  5593  mpt0  6663  naddrid  8654  ixp0x  8908  ac6sfi  9228  sup0riota  9412  infpssrlem4  10263  axdc3lem4  10410  0tsk  10713  uzsupss  12941  xrsupsslem  13310  xrinfmsslem  13311  xrsup0  13326  fsuppmapnn0fiubex  14005  swrd0  14672  swrdspsleq  14679  repswsymballbi  14793  cshw1  14835  rexfiuz  15375  lcmf0  16668  2prm  16726  0ssc  17870  0subcat  17871  drsdirfi  18337  0pos  18353  mrelatglb0  18593  s1chn  18652  chnub  18654  sgrp0b  18762  ga0  19338  psgnunilem3  19536  lbsexg  21231  ocv0  21726  mdetunilem9  22677  imasdsf1olem  24430  prdsxmslem2  24586  lebnumlem3  25022  cniccbdd  25520  ovolicc2lem4  25579  c1lip1  26056  ulm0  26451  rightge0  27911  precsexlem9  28305  onsbnd  28371  n0fincut  28445  zcuts  28497  twocut  28513  addhalfcut  28549  0reno  28586  istrkg2ld  28626  nbgr1vtx  29556  cplgr0  29623  cplgr1v  29628  wwlksn0s  30058  clwwlkn  30225  clwwlkn1  30240  0ewlk  30313  1ewlk  30314  0wlk  30315  0conngr  30391  frgr0v  30461  frgr0  30464  frgr1v  30470  1vwmgr  30475  chocnul  31528  locfinref  34135  esumnul  34342  derang0  35516  unt0  36058  nmulr0  36542  fdc  38241  lub0N  39810  glb0N  39814  0psubN  40370  sticksstones11  42770  cantnfresb  43898  safesnsupfilb  43991  nla0002  43997  nla0003  43998  iso0  44880  fnchoice  45606  eliuniincex  45684  eliincex  45685  limcdm0  46191  2ffzoeq  47919  iccpartiltu  48025  iccpartigtl  48026  0mgm  48785  linds0  49084  0funcALT  49706  0thincg  50076  termolmd  50288