ral0 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ral0		Structured version Visualization version Unicode version

Theorem ral0 4076

Description: Vacuous universal quantification is always true. (Contributed by NM, 20-Oct-2005.)

**Assertion**
Ref	Expression
ral0

**Proof of Theorem ral0**
Step	Hyp	Ref	Expression
1		noel 3919	. . 3
2	1	pm2.21i 116	. 2
3	2	rgen 2922	1

Colors of variables: wff setvar class

Syntax hints:

wcel 1990

wral 2912

c0 3915

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-v 3202 df-dif 3577 df-nul 3916

This theorem is referenced by: int0 4490 0iin 4578 po0 5050 so0 5068 mpt0 6021 ixp0x 7936 ac6sfi 8204 sup0riota 8371 infpssrlem4 9128 axdc3lem4 9275 0tsk 9577 uzsupss 11780 xrsupsslem 12137 xrinfmsslem 12138 xrsup0 12153 fsuppmapnn0fiubex 12792 swrd0 13434 swrdspsleq 13449 repswsymballbi 13527 cshw1 13568 rexfiuz 14087 lcmf0 15347 2prm 15405 0ssc 16497 0subcat 16498 drsdirfi 16938 0pos 16954 mrelatglb0 17185 sgrp0b 17292 ga0 17731 psgnunilem3 17916 lbsexg 19164 ocv0 20021 mdetunilem9 20426 imasdsf1olem 22178 prdsxmslem2 22334 lebnumlem3 22762 cniccbdd 23230 ovolicc2lem4 23288 c1lip1 23760 ulm0 24145 istrkg2ld 25359 nbgr0vtx 26252 nbgr1vtx 26254 uvtxa01vtx0 26297 cplgr0 26321 cplgr1v 26326 wwlksn0s 26746 0ewlk 26975 1ewlk 26976 0wlk 26977 0conngr 27052 frgr0v 27125 frgr0 27128 frgr1v 27135 1vwmgr 27140 chocnul 28187 locfinref 29908 esumnul 30110 derang0 31151 unt0 31588 nulsslt 31908 nulssgt 31909 fdc 33541 lub0N 34476 glb0N 34480 0psubN 35035 iso0 38506 fnchoice 39188 eliuniincex 39292 eliincex 39293 limcdm0 39850 2ffzoeq 41338 iccpartiltu 41358 iccpartigtl 41359 0mgm 41774 linds0 42254