![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ral0 | Structured version Visualization version Unicode version |
Description: Vacuous universal quantification is always true. (Contributed by NM, 20-Oct-2005.) |
Ref | Expression |
---|---|
ral0 |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | noel 3734 |
. . 3
![]() ![]() ![]() ![]() ![]() | |
2 | 1 | pm2.21i 135 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | rgen 2746 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ral 2741 df-v 3046 df-dif 3406 df-nul 3731 |
This theorem is referenced by: 0iin 4335 po0 4769 so0 4787 mpt0 5703 ixp0x 7547 ac6sfi 7812 sup0riota 7976 infpssrlem4 8733 axdc3lem4 8880 0tsk 9177 uzsupss 11253 xrsupsslem 11589 xrinfmsslem 11590 xrsup0 11606 fsuppmapnn0fiubex 12201 swrd0 12785 swrdspsleq 12800 repswsymballbi 12878 cshw1 12916 rexfiuz 13403 lcmf0 14600 2prm 14633 0ssc 15735 0subcat 15736 drsdirfi 16176 0pos 16193 mrelatglb0 16424 ga0 16945 psgnunilem3 17130 lbsexg 18380 ocv0 19233 mdetunilem9 19638 imasdsf1olem 21381 prdsxmslem2 21537 lebnumlem3 21984 lebnumlem3OLD 21987 cniccbdd 22405 ovolicc2lem4OLD 22466 ovolicc2lem4 22467 c1lip1 22942 ulm0 23339 istrkg2ld 24501 cusgra0v 25181 cusgra1v 25182 uvtx0 25212 0wlk 25268 0trl 25269 0conngra 25395 wwlkn0s 25426 0vgrargra 25658 eupa0 25695 frgra0v 25714 frgra1v 25719 1vwmgra 25724 chocnul 26974 locfinref 28661 esumnul 28862 derang0 29885 unt0 30331 nofulllem1 30584 fdc 32067 lub0N 32749 glb0N 32753 0psubN 33308 iso0 36649 fnchoice 37344 limcdm0 37692 iccpartiltu 38730 iccpartigtl 38731 2ffzoeq 39051 nbgr0vtx 39407 nbgr1vtx 39409 uvtxa01vtx0 39452 cplgr0 39476 cplgr0v 39478 cplgr1v 39480 0ewlk 39605 1ewlk 39607 01wlk 39647 0mgm 39761 linds0 40245 |
Copyright terms: Public domain | W3C validator |