Theorem ral0 4451

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

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

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

Syntax hints:   = wceq 1541  ∀wral 3051  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-ral 3052  df-dif 3904  df-nul 4286

This theorem is referenced by:  int0  4917  0iin  5019  po0  5549  so0  5570  mpt0  6634  naddrid  8611  ixp0x  8864  ac6sfi  9184  sup0riota  9369  infpssrlem4  10216  axdc3lem4  10363  0tsk  10666  uzsupss  12853  xrsupsslem  13222  xrinfmsslem  13223  xrsup0  13238  fsuppmapnn0fiubex  13915  swrd0  14582  swrdspsleq  14589  repswsymballbi  14703  cshw1  14745  rexfiuz  15271  lcmf0  16561  2prm  16619  0ssc  17761  0subcat  17762  drsdirfi  18228  0pos  18244  mrelatglb0  18484  s1chn  18543  chnub  18545  sgrp0b  18653  ga0  19227  psgnunilem3  19425  lbsexg  21119  ocv0  21632  mdetunilem9  22564  imasdsf1olem  24317  prdsxmslem2  24473  lebnumlem3  24918  cniccbdd  25418  ovolicc2lem4  25477  c1lip1  25958  ulm0  26356  rightge0  27817  precsexlem9  28211  onsbnd  28277  n0fincut  28351  zcuts  28403  twocut  28419  addhalfcut  28455  0reno  28492  istrkg2ld  28532  nbgr1vtx  29431  cplgr0  29498  cplgr1v  29503  wwlksn0s  29934  clwwlkn  30101  clwwlkn1  30116  0ewlk  30189  1ewlk  30190  0wlk  30191  0conngr  30267  frgr0v  30337  frgr0  30340  frgr1v  30346  1vwmgr  30351  chocnul  31403  locfinref  33998  esumnul  34205  derang0  35363  unt0  35905  fdc  37946  lub0N  39449  glb0N  39453  0psubN  40009  sticksstones11  42410  cantnfresb  43566  safesnsupfilb  43659  nla0002  43665  nla0003  43666  iso0  44548  fnchoice  45274  eliuniincex  45353  eliincex  45354  limcdm0  45864  2ffzoeq  47573  iccpartiltu  47668  iccpartigtl  47669  0mgm  48412  linds0  48711  0funcALT  49333  0thincg  49703  termolmd  49915