![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rzal | Structured version Visualization version GIF 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 4119 | . . . 4 ⊢ (𝑥 ∈ 𝐴 → 𝐴 ≠ ∅) | |
2 | 1 | necon2bi 2999 | . . 3 ⊢ (𝐴 = ∅ → ¬ 𝑥 ∈ 𝐴) |
3 | 2 | pm2.21d 119 | . 2 ⊢ (𝐴 = ∅ → (𝑥 ∈ 𝐴 → 𝜑)) |
4 | 3 | ralrimiv 3144 | 1 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1653 ∈ wcel 2157 ∀wral 3087 ∅c0 4113 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2775 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2784 df-cleq 2790 df-clel 2793 df-nfc 2928 df-ne 2970 df-ral 3092 df-v 3385 df-dif 3770 df-nul 4114 |
This theorem is referenced by: ralidm 4266 raaan 4271 iinrab2 4771 riinrab 4784 reusv2lem2 5067 cnvpo 5890 dffi3 8577 brdom3 9636 dedekind 10488 fimaxre2 11259 mgm0 17567 sgrp0 17603 efgs1 18458 opnnei 21250 axcontlem12 26204 nbgr0edg 26587 cplgr0v 26669 0vtxrgr 26818 0vconngr 27529 frgr1v 27612 ubthlem1 28243 matunitlindf 33888 mbfresfi 33936 bddiblnc 33960 blbnd 34065 rrnequiv 34113 upbdrech2 40255 fiminre2 40326 limsupubuz 40677 stoweidlem9 40957 fourierdlem31 41086 raaan2 41901 |
Copyright terms: Public domain | W3C validator |