Theorem ral0 4439

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

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

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

Syntax hints:   = wceq 1542  ∀wral 3052  ∅c0 4274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-ral 3053  df-dif 3893  df-nul 4275

This theorem is referenced by:  int0  4905  0iin  5007  po0  5550  so0  5571  mpt0  6635  naddrid  8613  ixp0x  8868  ac6sfi  9188  sup0riota  9373  infpssrlem4  10222  axdc3lem4  10369  0tsk  10672  uzsupss  12884  xrsupsslem  13253  xrinfmsslem  13254  xrsup0  13269  fsuppmapnn0fiubex  13948  swrd0  14615  swrdspsleq  14622  repswsymballbi  14736  cshw1  14778  rexfiuz  15304  lcmf0  16597  2prm  16655  0ssc  17798  0subcat  17799  drsdirfi  18265  0pos  18281  mrelatglb0  18521  s1chn  18580  chnub  18582  sgrp0b  18690  ga0  19267  psgnunilem3  19465  lbsexg  21157  ocv0  21670  mdetunilem9  22598  imasdsf1olem  24351  prdsxmslem2  24507  lebnumlem3  24943  cniccbdd  25441  ovolicc2lem4  25500  c1lip1  25977  ulm0  26372  rightge0  27830  precsexlem9  28224  onsbnd  28290  n0fincut  28364  zcuts  28416  twocut  28432  addhalfcut  28468  0reno  28505  istrkg2ld  28545  nbgr1vtx  29444  cplgr0  29511  cplgr1v  29516  wwlksn0s  29947  clwwlkn  30114  clwwlkn1  30129  0ewlk  30202  1ewlk  30203  0wlk  30204  0conngr  30280  frgr0v  30350  frgr0  30353  frgr1v  30359  1vwmgr  30364  chocnul  31417  locfinref  34004  esumnul  34211  derang0  35370  unt0  35912  fdc  38083  lub0N  39652  glb0N  39656  0psubN  40212  sticksstones11  42612  cantnfresb  43773  safesnsupfilb  43866  nla0002  43872  nla0003  43873  iso0  44755  fnchoice  45481  eliuniincex  45560  eliincex  45561  limcdm0  46069  2ffzoeq  47791  iccpartiltu  47897  iccpartigtl  47898  0mgm  48657  linds0  48956  0funcALT  49578  0thincg  49948  termolmd  50160