![]() |
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.) Avoid df-clel 2813, ax-8 2107. (Revised by GG, 2-Sep-2024.) |
Ref | Expression |
---|---|
rzal | ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfcleq 2727 | . . . 4 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥})) | |
2 | 1 | biimpi 216 | . . 3 ⊢ (𝐴 = {𝑦 ∣ ⊥} → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥})) |
3 | df-clab 2712 | . . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥) | |
4 | sbv 2085 | . . . . . 6 ⊢ ([𝑥 / 𝑦]⊥ ↔ ⊥) | |
5 | 3, 4 | bitri 275 | . . . . 5 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ ⊥) |
6 | 5 | bibi2i 337 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ (𝑥 ∈ 𝐴 ↔ ⊥)) |
7 | nbfal 1551 | . . . . 5 ⊢ (¬ 𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ↔ ⊥)) | |
8 | pm2.21 123 | . . . . 5 ⊢ (¬ 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 → 𝜑)) | |
9 | 7, 8 | sylbir 235 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ ⊥) → (𝑥 ∈ 𝐴 → 𝜑)) |
10 | 6, 9 | sylbi 217 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) → (𝑥 ∈ 𝐴 → 𝜑)) |
11 | 2, 10 | sylg 1819 | . 2 ⊢ (𝐴 = {𝑦 ∣ ⊥} → ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
12 | dfnul4 4340 | . . 3 ⊢ ∅ = {𝑦 ∣ ⊥} | |
13 | 12 | eqeq2i 2747 | . 2 ⊢ (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥}) |
14 | df-ral 3059 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
15 | 11, 13, 14 | 3imtr4i 292 | 1 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∀wal 1534 = wceq 1536 ⊥wfal 1548 [wsb 2061 ∈ wcel 2105 {cab 2711 ∀wral 3058 ∅c0 4338 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-9 2115 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1539 df-fal 1549 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-ral 3059 df-dif 3965 df-nul 4339 |
This theorem is referenced by: rexn0 4516 ral0 4518 ralf0 4519 raaan 4522 raaanv 4523 raaan2 4526 iinrab2 5074 riinrab 5088 reusv2lem2 5404 cnvpo 6308 dffi3 9468 brdom3 10565 dedekind 11421 fimaxre2 12210 fiminre2 12213 mgm0 18681 sgrp0 18752 efgs1 19767 opnnei 23143 bddiblnc 25891 axcontlem12 29004 nbgr0edg 29388 prcliscplgr 29445 cplgr0v 29458 0vtxrgr 29608 0vconngr 30221 frgr1v 30299 ubthlem1 30898 rdgssun 37360 matunitlindf 37604 mbfresfi 37652 blbnd 37773 rrnequiv 37821 upbdrech2 45258 limsupubuz 45668 stoweidlem9 45964 fourierdlem31 46093 upwordnul 46833 upwordsing 46837 |
Copyright terms: Public domain | W3C validator |