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

Theorem rzal 4502
Description: Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) Avoid df-clel 2809, ax-8 2108. (Revised by Gino Giotto, 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 2724 . . . 4 (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥𝐴𝑥 ∈ {𝑦 ∣ ⊥}))
21biimpi 215 . . 3 (𝐴 = {𝑦 ∣ ⊥} → ∀𝑥(𝑥𝐴𝑥 ∈ {𝑦 ∣ ⊥}))
3 df-clab 2709 . . . . . 6 (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
4 sbv 2091 . . . . . 6 ([𝑥 / 𝑦]⊥ ↔ ⊥)
53, 4bitri 274 . . . . 5 (𝑥 ∈ {𝑦 ∣ ⊥} ↔ ⊥)
65bibi2i 337 . . . 4 ((𝑥𝐴𝑥 ∈ {𝑦 ∣ ⊥}) ↔ (𝑥𝐴 ↔ ⊥))
7 nbfal 1556 . . . . 5 𝑥𝐴 ↔ (𝑥𝐴 ↔ ⊥))
8 pm2.21 123 . . . . 5 𝑥𝐴 → (𝑥𝐴𝜑))
97, 8sylbir 234 . . . 4 ((𝑥𝐴 ↔ ⊥) → (𝑥𝐴𝜑))
106, 9sylbi 216 . . 3 ((𝑥𝐴𝑥 ∈ {𝑦 ∣ ⊥}) → (𝑥𝐴𝜑))
112, 10sylg 1825 . 2 (𝐴 = {𝑦 ∣ ⊥} → ∀𝑥(𝑥𝐴𝜑))
12 dfnul4 4320 . . 3 ∅ = {𝑦 ∣ ⊥}
1312eqeq2i 2744 . 2 (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥})
14 df-ral 3061 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
1511, 13, 143imtr4i 291 1 (𝐴 = ∅ → ∀𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wal 1539   = wceq 1541  wfal 1553  [wsb 2067  wcel 2106  {cab 2708  wral 3060  c0 4318
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-ral 3061  df-dif 3947  df-nul 4319
This theorem is referenced by:  rexn0  4504  ral0  4506  ralf0  4507  ralidmOLD  4509  raaan  4514  raaanv  4515  raaan2  4518  iinrab2  5066  riinrab  5080  reusv2lem2  5390  cnvpo  6275  dffi3  9408  brdom3  10505  dedekind  11359  fimaxre2  12141  fiminre2  12144  mgm0  18557  sgrp0  18599  efgs1  19567  opnnei  22553  bddiblnc  25288  axcontlem12  28098  nbgr0edg  28479  prcliscplgr  28536  cplgr0v  28549  0vtxrgr  28698  0vconngr  29311  frgr1v  29389  ubthlem1  29986  rdgssun  36061  matunitlindf  36288  mbfresfi  36336  blbnd  36458  rrnequiv  36506  upbdrech2  43789  limsupubuz  44200  stoweidlem9  44496  fourierdlem31  44625  upwordnul  45365  upwordsing  45369
  Copyright terms: Public domain W3C validator