MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rzal Structured version   Visualization version   GIF version

Theorem rzal 4509
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.)
Assertion
Ref Expression
rzal (𝐴 = ∅ → ∀𝑥𝐴 𝜑)
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rzal
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 dfcleq 2730 . . . 4 (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥𝐴𝑥 ∈ {𝑦 ∣ ⊥}))
21biimpi 216 . . 3 (𝐴 = {𝑦 ∣ ⊥} → ∀𝑥(𝑥𝐴𝑥 ∈ {𝑦 ∣ ⊥}))
3 df-clab 2715 . . . . . 6 (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
4 sbv 2088 . . . . . 6 ([𝑥 / 𝑦]⊥ ↔ ⊥)
53, 4bitri 275 . . . . 5 (𝑥 ∈ {𝑦 ∣ ⊥} ↔ ⊥)
65bibi2i 337 . . . 4 ((𝑥𝐴𝑥 ∈ {𝑦 ∣ ⊥}) ↔ (𝑥𝐴 ↔ ⊥))
7 nbfal 1555 . . . . 5 𝑥𝐴 ↔ (𝑥𝐴 ↔ ⊥))
8 pm2.21 123 . . . . 5 𝑥𝐴 → (𝑥𝐴𝜑))
97, 8sylbir 235 . . . 4 ((𝑥𝐴 ↔ ⊥) → (𝑥𝐴𝜑))
106, 9sylbi 217 . . 3 ((𝑥𝐴𝑥 ∈ {𝑦 ∣ ⊥}) → (𝑥𝐴𝜑))
112, 10sylg 1823 . 2 (𝐴 = {𝑦 ∣ ⊥} → ∀𝑥(𝑥𝐴𝜑))
12 dfnul4 4335 . . 3 ∅ = {𝑦 ∣ ⊥}
1312eqeq2i 2750 . 2 (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥})
14 df-ral 3062 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
1511, 13, 143imtr4i 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