Theorem ral0 4513

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

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

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

Syntax hints:   = wceq 1540  ∀wral 3061  ∅c0 4333

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-ral 3062  df-dif 3954  df-nul 4334

This theorem is referenced by:  int0  4962  0iin  5064  po0  5609  so0  5630  mpt0  6710  naddrid  8721  ixp0x  8966  ac6sfi  9320  sup0riota  9505  infpssrlem4  10346  axdc3lem4  10493  0tsk  10795  uzsupss  12982  xrsupsslem  13349  xrinfmsslem  13350  xrsup0  13365  fsuppmapnn0fiubex  14033  swrd0  14696  swrdspsleq  14703  repswsymballbi  14818  cshw1  14860  rexfiuz  15386  lcmf0  16671  2prm  16729  0ssc  17882  0subcat  17883  drsdirfi  18351  0pos  18367  mrelatglb0  18606  sgrp0b  18741  ga0  19316  psgnunilem3  19514  lbsexg  21166  ocv0  21695  mdetunilem9  22626  imasdsf1olem  24383  prdsxmslem2  24542  lebnumlem3  24995  cniccbdd  25496  ovolicc2lem4  25555  c1lip1  26036  ulm0  26434  precsexlem9  28239  zscut  28393  nohalf  28407  addhalfcut  28419  istrkg2ld  28468  nbgr1vtx  29375  cplgr0  29442  cplgr1v  29447  wwlksn0s  29881  clwwlkn  30045  clwwlkn1  30060  0ewlk  30133  1ewlk  30134  0wlk  30135  0conngr  30211  frgr0v  30281  frgr0  30284  frgr1v  30290  1vwmgr  30295  chocnul  31347  s1chn  33000  chnub  33002  locfinref  33840  esumnul  34049  derang0  35174  unt0  35711  fdc  37752  lub0N  39190  glb0N  39194  0psubN  39751  sticksstones11  42157  cantnfresb  43337  safesnsupfilb  43431  nla0002  43437  nla0003  43438  iso0  44326  fnchoice  45034  eliuniincex  45114  eliincex  45115  limcdm0  45633  2ffzoeq  47339  iccpartiltu  47409  iccpartigtl  47410  0mgm  48082  linds0  48382  0funcALT  48921  0thincg  49107