| 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 2816, ax-8 2110. (Revised by GG, 2-Sep-2024.) |
| Ref | Expression |
|---|---|
| rzal | ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfcleq 2730 | . . . 4 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥})) | |
| 2 | 1 | biimpi 216 | . . 3 ⊢ (𝐴 = {𝑦 ∣ ⊥} → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥})) |
| 3 | df-clab 2715 | . . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥) | |
| 4 | sbv 2088 | . . . . . 6 ⊢ ([𝑥 / 𝑦]⊥ ↔ ⊥) | |
| 5 | 3, 4 | bitri 275 | . . . . 5 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ ⊥) |
| 6 | 5 | bibi2i 337 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ (𝑥 ∈ 𝐴 ↔ ⊥)) |
| 7 | nbfal 1555 | . . . . 5 ⊢ (¬ 𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ↔ ⊥)) | |
| 8 | pm2.21 123 | . . . . 5 ⊢ (¬ 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 → 𝜑)) | |
| 9 | 7, 8 | sylbir 235 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ ⊥) → (𝑥 ∈ 𝐴 → 𝜑)) |
| 10 | 6, 9 | sylbi 217 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) → (𝑥 ∈ 𝐴 → 𝜑)) |
| 11 | 2, 10 | sylg 1823 | . 2 ⊢ (𝐴 = {𝑦 ∣ ⊥} → ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
| 12 | dfnul4 4335 | . . 3 ⊢ ∅ = {𝑦 ∣ ⊥} | |
| 13 | 12 | eqeq2i 2750 | . 2 ⊢ (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥}) |
| 14 | df-ral 3062 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
| 15 | 11, 13, 14 | 3imtr4i 292 | 1 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∀wal 1538 = wceq 1540 ⊥wfal 1552 [wsb 2064 ∈ wcel 2108 {cab 2714 ∀wral 3061 ∅c0 4333 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-ral 3062 df-dif 3954 df-nul 4334 |
| This theorem is referenced by: rexn0 4511 ral0 4513 ralf0 4514 raaan 4517 raaanv 4518 raaan2 4521 iinrab2 5070 riinrab 5084 reusv2lem2 5399 cnvpo 6307 dffi3 9471 brdom3 10568 dedekind 11424 fimaxre2 12213 fiminre2 12216 mgm0 18669 sgrp0 18740 efgs1 19753 opnnei 23128 bddiblnc 25877 axcontlem12 28990 nbgr0edg 29374 prcliscplgr 29431 cplgr0v 29444 0vtxrgr 29594 0vconngr 30212 frgr1v 30290 ubthlem1 30889 rdgssun 37379 matunitlindf 37625 mbfresfi 37673 blbnd 37794 rrnequiv 37842 upbdrech2 45320 limsupubuz 45728 stoweidlem9 46024 fourierdlem31 46153 upwordnul 46895 upwordsing 46899 0funcg2 48917 |
| Copyright terms: Public domain | W3C validator |