Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ral0 | Structured version Visualization version GIF version |
Description: Vacuous universal quantification is always true. (Contributed by NM, 20-Oct-2005.) |
Ref | Expression |
---|---|
ral0 | ⊢ ∀𝑥 ∈ ∅ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | noel 3878 | . . 3 ⊢ ¬ 𝑥 ∈ ∅ | |
2 | 1 | pm2.21i 115 | . 2 ⊢ (𝑥 ∈ ∅ → 𝜑) |
3 | 2 | rgen 2906 | 1 ⊢ ∀𝑥 ∈ ∅ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 1977 ∀wral 2896 ∅c0 3874 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-v 3175 df-dif 3543 df-nul 3875 |
This theorem is referenced by: int0 4425 0iin 4514 po0 4974 so0 4992 mpt0 5934 ixp0x 7822 ac6sfi 8089 sup0riota 8254 infpssrlem4 9011 axdc3lem4 9158 0tsk 9456 uzsupss 11656 xrsupsslem 12009 xrinfmsslem 12010 xrsup0 12025 fsuppmapnn0fiubex 12654 swrd0 13286 swrdspsleq 13301 repswsymballbi 13378 cshw1 13419 rexfiuz 13935 lcmf0 15185 2prm 15243 0ssc 16320 0subcat 16321 drsdirfi 16761 0pos 16777 mrelatglb0 17008 mgm0 17078 sgrp0 17114 sgrp0b 17115 ga0 17554 psgnunilem3 17739 lbsexg 18985 ocv0 19840 mdetunilem9 20245 imasdsf1olem 21988 prdsxmslem2 22144 lebnumlem3 22570 cniccbdd 23037 ovolicc2lem4 23095 c1lip1 23564 ulm0 23949 istrkg2ld 25159 cusgra0v 25989 cusgra1v 25990 uvtx0 26019 0wlk 26075 0trl 26076 0conngra 26202 wwlkn0s 26233 0vgrargra 26464 eupa0 26501 frgra0v 26520 frgra1v 26525 1vwmgra 26530 chocnul 27571 locfinref 29236 esumnul 29437 derang0 30405 unt0 30842 nofulllem1 31101 fdc 32711 lub0N 33494 glb0N 33498 0psubN 34053 iso0 37528 fnchoice 38211 eliuniincex 38323 eliincex 38324 limcdm0 38685 iccpartiltu 39960 iccpartigtl 39961 2ffzoeq 40361 nbgr0vtx 40578 nbgr1vtx 40580 uvtxa01vtx0 40623 cplgr0 40647 cplgr0v 40649 cplgr1v 40652 wwlksn0s 41057 0ewlk 41282 1ewlk 41283 01wlk 41284 0conngr 41359 0vconngr 41360 frgr0v 41433 frgr0 41436 frgr1v 41441 1vwmgr 41446 0mgm 41564 linds0 42048 |
Copyright terms: Public domain | W3C validator |