Theorem ral0 4506

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

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

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

Syntax hints:   = wceq 1541  ∀wral 3060  ∅c0 4318

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-ral 3061  df-dif 3947  df-nul 4319

This theorem is referenced by:  int0  4959  0iin  5060  po0  5598  so0  5617  mpt0  6679  naddrid  8665  ixp0x  8903  ac6sfi  9270  sup0riota  9442  infpssrlem4  10283  axdc3lem4  10430  0tsk  10732  uzsupss  12906  xrsupsslem  13268  xrinfmsslem  13269  xrsup0  13284  fsuppmapnn0fiubex  13939  swrd0  14590  swrdspsleq  14597  repswsymballbi  14712  cshw1  14754  rexfiuz  15276  lcmf0  16553  2prm  16611  0ssc  17769  0subcat  17770  drsdirfi  18240  0pos  18256  0posOLD  18257  mrelatglb0  18496  sgrp0b  18600  ga0  19128  psgnunilem3  19328  lbsexg  20726  ocv0  21163  mdetunilem9  22051  imasdsf1olem  23808  prdsxmslem2  23967  lebnumlem3  24408  cniccbdd  24907  ovolicc2lem4  24966  c1lip1  25443  ulm0  25832  istrkg2ld  27576  nbgr0vtx  28478  nbgr1vtx  28480  cplgr0  28547  cplgr1v  28552  wwlksn0s  28980  clwwlkn  29144  clwwlkn1  29159  0ewlk  29232  1ewlk  29233  0wlk  29234  0conngr  29310  frgr0v  29380  frgr0  29383  frgr1v  29389  1vwmgr  29394  chocnul  30444  locfinref  32652  esumnul  32877  derang0  33991  unt0  34510  fdc  36418  lub0N  37864  glb0N  37868  0psubN  38425  sticksstones11  40777  cantnfresb  41845  safesnsupfilb  41940  nla0002  41946  nla0003  41947  iso0  42837  fnchoice  43484  eliuniincex  43569  eliincex  43570  limcdm0  44107  2ffzoeq  45808  iccpartiltu  45862  iccpartigtl  45863  0mgm  46316  linds0  46794  0thincg  47318