![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rzal | Structured version Visualization version Unicode version |
Description: Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Ref | Expression |
---|---|
rzal |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ne0i 3736 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | necon2bi 2653 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | pm2.21d 110 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | ralrimiv 2799 |
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-ne 2623 df-ral 2741 df-v 3046 df-dif 3406 df-nul 3731 |
This theorem is referenced by: ralidm 3872 rgenz 3874 ralf0 3875 raaan 3876 raaanv 3877 iinrab2 4340 riinrab 4353 reusv2lem2 4604 cnvpo 5373 dffi3 7942 brdom3 8953 dedekind 9794 fimaxre2 10549 efgs1 17378 opnnei 20129 axcontlem12 24998 ubthlem1 26505 nofulllem2 30585 mbfresfi 31980 bddiblnc 32005 blbnd 32112 rrnequiv 32160 upbdrech2 37520 stoweidlem9 37863 fourierdlem31 37994 fourierdlem31OLD 37995 raaan2 38590 nbgr0edg 39408 0vtxrgr 39575 |
Copyright terms: Public domain | W3C validator |