Theorem ral0 4426

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

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

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

Syntax hints:   = wceq 1547  ∀wral 3053  ∅c0 4261

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-ral 3054  df-dif 3886  df-nul 4262

This theorem is referenced by:  int0  4892  0iin  4993  po0  5543  so0  5564  mpt0  6627  naddrid  8609  ixp0x  8864  ac6sfi  9184  sup0riota  9369  infpssrlem4  10219  axdc3lem4  10366  0tsk  10669  uzsupss  12881  xrsupsslem  13250  xrinfmsslem  13251  xrsup0  13266  fsuppmapnn0fiubex  13945  swrd0  14612  swrdspsleq  14619  repswsymballbi  14733  cshw1  14775  rexfiuz  15301  lcmf0  16594  2prm  16652  0ssc  17795  0subcat  17796  drsdirfi  18262  0pos  18278  mrelatglb0  18518  s1chn  18577  chnub  18579  sgrp0b  18687  ga0  19264  psgnunilem3  19462  lbsexg  21157  ocv0  21652  mdetunilem9  22603  imasdsf1olem  24356  prdsxmslem2  24512  lebnumlem3  24948  cniccbdd  25446  ovolicc2lem4  25505  c1lip1  25982  ulm0  26374  rightge0  27831  precsexlem9  28225  onsbnd  28291  n0fincut  28365  zcuts  28417  twocut  28433  addhalfcut  28469  0reno  28506  istrkg2ld  28546  nbgr1vtx  29445  cplgr0  29512  cplgr1v  29517  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  34025  esumnul  34232  derang0  35397  unt0  35939  fdc  38112  lub0N  39681  glb0N  39685  0psubN  40241  sticksstones11  42641  cantnfresb  43769  safesnsupfilb  43862  nla0002  43868  nla0003  43869  iso0  44751  fnchoice  45477  eliuniincex  45556  eliincex  45557  limcdm0  46063  2ffzoeq  47791  iccpartiltu  47897  iccpartigtl  47898  0mgm  48657  linds0  48956  0funcALT  49578  0thincg  49948  termolmd  50160