Theorem ral0 4513

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

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

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

Syntax hints:   = wceq 1534  ∀wral 3058  ∅c0 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-ral 3059  df-dif 3950  df-nul 4324

This theorem is referenced by:  int0  4965  0iin  5067  po0  5607  so0  5626  mpt0  6697  naddrid  8704  ixp0x  8945  ac6sfi  9312  sup0riota  9489  infpssrlem4  10330  axdc3lem4  10477  0tsk  10779  uzsupss  12955  xrsupsslem  13319  xrinfmsslem  13320  xrsup0  13335  fsuppmapnn0fiubex  13990  swrd0  14641  swrdspsleq  14648  repswsymballbi  14763  cshw1  14805  rexfiuz  15327  lcmf0  16605  2prm  16663  0ssc  17823  0subcat  17824  drsdirfi  18297  0pos  18313  0posOLD  18314  mrelatglb0  18553  sgrp0b  18688  ga0  19249  psgnunilem3  19451  lbsexg  21052  ocv0  21609  mdetunilem9  22535  imasdsf1olem  24292  prdsxmslem2  24451  lebnumlem3  24902  cniccbdd  25403  ovolicc2lem4  25462  c1lip1  25943  ulm0  26340  precsexlem9  28126  istrkg2ld  28277  nbgr0vtx  29182  nbgr1vtx  29184  cplgr0  29251  cplgr1v  29256  wwlksn0s  29685  clwwlkn  29849  clwwlkn1  29864  0ewlk  29937  1ewlk  29938  0wlk  29939  0conngr  30015  frgr0v  30085  frgr0  30088  frgr1v  30094  1vwmgr  30099  chocnul  31151  locfinref  33442  esumnul  33667  derang0  34779  unt0  35305  fdc  37218  lub0N  38661  glb0N  38665  0psubN  39222  sticksstones11  41628  cantnfresb  42753  safesnsupfilb  42848  nla0002  42854  nla0003  42855  iso0  43744  fnchoice  44391  eliuniincex  44475  eliincex  44476  limcdm0  45006  2ffzoeq  46708  iccpartiltu  46762  iccpartigtl  46763  0mgm  47228  linds0  47533  0thincg  48056