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

Theorem rzal 4264
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 4119 . . . 4 (𝑥𝐴𝐴 ≠ ∅)
21necon2bi 2999 . . 3 (𝐴 = ∅ → ¬ 𝑥𝐴)
32pm2.21d 119 . 2 (𝐴 = ∅ → (𝑥𝐴𝜑))
43ralrimiv 3144 1 (𝐴 = ∅ → ∀𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1653  wcel 2157  wral 3087  c0 4113
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2775
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-ne 2970  df-ral 3092  df-v 3385  df-dif 3770  df-nul 4114
This theorem is referenced by:  ralidm  4266  raaan  4271  iinrab2  4771  riinrab  4784  reusv2lem2  5067  cnvpo  5890  dffi3  8577  brdom3  9636  dedekind  10488  fimaxre2  11259  mgm0  17567  sgrp0  17603  efgs1  18458  opnnei  21250  axcontlem12  26204  nbgr0edg  26587  cplgr0v  26669  0vtxrgr  26818  0vconngr  27529  frgr1v  27612  ubthlem1  28243  matunitlindf  33888  mbfresfi  33936  bddiblnc  33960  blbnd  34065  rrnequiv  34113  upbdrech2  40255  fiminre2  40326  limsupubuz  40677  stoweidlem9  40957  fourierdlem31  41086  raaan2  41901
  Copyright terms: Public domain W3C validator