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

Theorem rzal 4051
 Description: Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
rzal (𝐴 = ∅ → ∀𝑥𝐴 𝜑)
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rzal
StepHypRef Expression
1 ne0i 3903 . . . 4 (𝑥𝐴𝐴 ≠ ∅)
21necon2bi 2820 . . 3 (𝐴 = ∅ → ¬ 𝑥𝐴)
32pm2.21d 118 . 2 (𝐴 = ∅ → (𝑥𝐴𝜑))
43ralrimiv 2961 1 (𝐴 = ∅ → ∀𝑥𝐴 𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1480   ∈ wcel 1987  ∀wral 2908  ∅c0 3897 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-v 3192  df-dif 3563  df-nul 3898 This theorem is referenced by:  ralidm  4053  rgenzOLD  4055  ralf0OLD  4057  raaan  4060  iinrab2  4556  riinrab  4569  reusv2lem2  4839  reusv2lem2OLD  4840  cnvpo  5642  dffi3  8297  brdom3  9310  dedekind  10160  fimaxre2  10929  mgm0  17195  sgrp0  17231  efgs1  18088  opnnei  20864  axcontlem12  25789  nbgr0edg  26174  cplgr0v  26244  0vtxrgr  26376  0vconngr  26953  frgr1v  27033  ubthlem1  27614  matunitlindf  33078  mbfresfi  33127  bddiblnc  33151  blbnd  33257  rrnequiv  33305  upbdrech2  39021  fiminre2  39093  limsupubuz  39381  stoweidlem9  39563  fourierdlem31  39692  raaan2  40509
 Copyright terms: Public domain W3C validator