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

Theorem rzal 4451
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 4299 . . . 4 (𝑥𝐴𝐴 ≠ ∅)
21necon2bi 3046 . . 3 (𝐴 = ∅ → ¬ 𝑥𝐴)
32pm2.21d 121 . 2 (𝐴 = ∅ → (𝑥𝐴𝜑))
43ralrimiv 3181 1 (𝐴 = ∅ → ∀𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105  wral 3138  c0 4290
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-ne 3017  df-ral 3143  df-dif 3938  df-nul 4291
This theorem is referenced by:  ralidm  4453  raaan  4458  raaanv  4459  raaan2  4462  iinrab2  4984  riinrab  4998  reusv2lem2  5291  cnvpo  6132  dffi3  8884  brdom3  9939  dedekind  10792  fimaxre2  11575  mgm0  17856  sgrp0  17898  efgs1  18792  opnnei  21658  axcontlem12  26689  nbgr0edg  27067  prcliscplgr  27124  cplgr0v  27137  0vtxrgr  27286  0vconngr  27900  frgr1v  27978  ubthlem1  28575  rdgssun  34542  matunitlindf  34772  mbfresfi  34820  bddiblnc  34844  blbnd  34948  rrnequiv  34996  upbdrech2  41455  fiminre2  41526  limsupubuz  41874  stoweidlem9  42175  fourierdlem31  42304
  Copyright terms: Public domain W3C validator