Theorem ral0 4459

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

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

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

Syntax hints:   = wceq 1570  ∀wral 3079  ∅c0 4286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-ral 3080  df-dif 3908  df-nul 4287

This theorem is referenced by:  int0  4927  0iin  5028  po0  5586  so0  5607  mpt0  6677  naddrid  8666  ixp0x  8920  ac6sfi  9240  sup0riota  9422  infpssrlem4  10285  axdc3lem4  10432  0tsk  10735  uzsupss  12959  xrsupsslem  13328  xrinfmsslem  13329  xrsup0  13344  fsuppmapnn0fiubex  14024  swrd0  14692  swrdspsleq  14699  repswsymballbi  14813  cshw1  14855  rexfiuz  15395  lcmf0  16687  2prm  16745  0ssc  17889  0subcat  17890  drsdirfi  18356  0pos  18372  mrelatglb0  18612  s1chn  18671  chnub  18673  sgrp0b  18781  ga0  19363  psgnunilem3  19561  lbsexg  21288  ocv0  21827  mdetunilem9  22777  imasdsf1olem  24530  prdsxmslem2  24686  lebnumlem3  25122  cniccbdd  25620  ovolicc2lem4  25679  c1lip1  26156  ulm0  26554  rightge0  28014  precsexlem9  28408  onsbnd  28474  n0fincut  28548  zcuts  28600  twocut  28616  addhalfcut  28652  0reno  28689  istrkg2ld  28729  nbgr1vtx  29708  cplgr0  29775  cplgr1v  29780  wwlksn0s  30210  clwwlkn  30377  clwwlkn1  30392  0ewlk  30465  1ewlk  30466  0wlk  30467  0conngr  30543  frgr0v  30613  frgr0  30616  frgr1v  30622  1vwmgr  30627  chocnul  31680  locfinref  34231  esumnul  34438  derang0  35661  unt0  36203  nmulr0  36687  fdc  38396  lub0N  39963  glb0N  39967  0psubN  40523  sticksstones11  42923  cantnfresb  44051  safesnsupfilb  44144  nla0002  44150  nla0003  44151  iso0  45017  fnchoice  45749  eliuniincex  45827  eliincex  45828  limcdm0  46334  2ffzoeq  48065  iccpartiltu  48171  iccpartigtl  48172  0mgm  48931  linds0  49245  0funcALT  49866  0thincg  50236  termolmd  50448