Theorem ral0 4475

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 4471	. 2 ⊢ (∅ = ∅ → ∀𝑥 ∈ ∅ 𝜑)
3	1, 2	ax-mp 5	1 ⊢ ∀𝑥 ∈ ∅ 𝜑

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

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 3916  df-nul 4288

This theorem is referenced by:  int0  4928  0iin  5029  po0  5567  so0  5586  mpt0  6648  naddrid  8634  ixp0x  8871  ac6sfi  9238  sup0riota  9410  infpssrlem4  10251  axdc3lem4  10398  0tsk  10700  uzsupss  12874  xrsupsslem  13236  xrinfmsslem  13237  xrsup0  13252  fsuppmapnn0fiubex  13907  swrd0  14558  swrdspsleq  14565  repswsymballbi  14680  cshw1  14722  rexfiuz  15244  lcmf0  16521  2prm  16579  0ssc  17737  0subcat  17738  drsdirfi  18208  0pos  18224  0posOLD  18225  mrelatglb0  18464  sgrp0b  18568  ga0  19092  psgnunilem3  19292  lbsexg  20684  ocv0  21118  mdetunilem9  22006  imasdsf1olem  23763  prdsxmslem2  23922  lebnumlem3  24363  cniccbdd  24862  ovolicc2lem4  24921  c1lip1  25398  ulm0  25787  istrkg2ld  27465  nbgr0vtx  28367  nbgr1vtx  28369  cplgr0  28436  cplgr1v  28441  wwlksn0s  28869  clwwlkn  29033  clwwlkn1  29048  0ewlk  29121  1ewlk  29122  0wlk  29123  0conngr  29199  frgr0v  29269  frgr0  29272  frgr1v  29278  1vwmgr  29283  chocnul  30333  locfinref  32511  esumnul  32736  derang0  33850  unt0  34369  fdc  36277  lub0N  37724  glb0N  37728  0psubN  38285  sticksstones11  40637  cantnfresb  41717  safesnsupfilb  41812  nla0002  41818  nla0003  41819  iso0  42709  fnchoice  43356  eliuniincex  43441  eliincex  43442  limcdm0  43979  2ffzoeq  45680  iccpartiltu  45734  iccpartigtl  45735  0mgm  46188  linds0  46666  0thincg  47190