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 4299 | . . . 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 1528 ∈ wcel 2105 ∀wral 3138 ∅c0 4290 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-ne 3017 df-ral 3143 df-dif 3938 df-nul 4291 |
This theorem is referenced by: ralidm 4453 raaan 4458 raaanv 4459 raaan2 4462 iinrab2 4984 riinrab 4998 reusv2lem2 5291 cnvpo 6132 dffi3 8884 brdom3 9939 dedekind 10792 fimaxre2 11575 mgm0 17856 sgrp0 17898 efgs1 18792 opnnei 21658 axcontlem12 26689 nbgr0edg 27067 prcliscplgr 27124 cplgr0v 27137 0vtxrgr 27286 0vconngr 27900 frgr1v 27978 ubthlem1 28575 rdgssun 34542 matunitlindf 34772 mbfresfi 34820 bddiblnc 34844 blbnd 34948 rrnequiv 34996 upbdrech2 41455 fiminre2 41526 limsupubuz 41874 stoweidlem9 42175 fourierdlem31 42304 |
Copyright terms: Public domain | W3C validator |