![]() |
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 4150 | . . . 4 ⊢ (𝑥 ∈ 𝐴 → 𝐴 ≠ ∅) | |
2 | 1 | necon2bi 3029 | . . 3 ⊢ (𝐴 = ∅ → ¬ 𝑥 ∈ 𝐴) |
3 | 2 | pm2.21d 119 | . 2 ⊢ (𝐴 = ∅ → (𝑥 ∈ 𝐴 → 𝜑)) |
4 | 3 | ralrimiv 3174 | 1 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1658 ∈ wcel 2166 ∀wral 3117 ∅c0 4144 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ne 3000 df-ral 3122 df-v 3416 df-dif 3801 df-nul 4145 |
This theorem is referenced by: ralidm 4297 raaan 4302 iinrab2 4803 riinrab 4816 reusv2lem2 5099 cnvpo 5914 dffi3 8606 brdom3 9665 dedekind 10519 fimaxre2 11299 mgm0 17608 sgrp0 17644 efgs1 18499 opnnei 21295 axcontlem12 26274 nbgr0edg 26654 cplgr0v 26725 0vtxrgr 26874 0vconngr 27569 frgr1v 27652 ubthlem1 28281 matunitlindf 33951 mbfresfi 33999 bddiblnc 34023 blbnd 34128 rrnequiv 34176 upbdrech2 40320 fiminre2 40391 limsupubuz 40740 stoweidlem9 41020 fourierdlem31 41149 raaan2 41961 |
Copyright terms: Public domain | W3C validator |