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 4300 | . . . 4 ⊢ (𝑥 ∈ 𝐴 → 𝐴 ≠ ∅) | |
2 | 1 | necon2bi 3046 | . . 3 ⊢ (𝐴 = ∅ → ¬ 𝑥 ∈ 𝐴) |
3 | 2 | pm2.21d 121 | . 2 ⊢ (𝐴 = ∅ → (𝑥 ∈ 𝐴 → 𝜑)) |
4 | 3 | ralrimiv 3181 | 1 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ∈ wcel 2114 ∀wral 3138 ∅c0 4291 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-ne 3017 df-ral 3143 df-dif 3939 df-nul 4292 |
This theorem is referenced by: ralidm 4455 raaan 4460 raaanv 4461 raaan2 4464 iinrab2 4992 riinrab 5006 reusv2lem2 5300 cnvpo 6138 dffi3 8895 brdom3 9950 dedekind 10803 fimaxre2 11586 mgm0 17866 sgrp0 17908 efgs1 18861 opnnei 21728 axcontlem12 26761 nbgr0edg 27139 prcliscplgr 27196 cplgr0v 27209 0vtxrgr 27358 0vconngr 27972 frgr1v 28050 ubthlem1 28647 rdgssun 34662 matunitlindf 34905 mbfresfi 34953 bddiblnc 34977 blbnd 35080 rrnequiv 35128 upbdrech2 41595 fiminre2 41666 limsupubuz 42014 stoweidlem9 42314 fourierdlem31 42443 |
Copyright terms: Public domain | W3C validator |