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

Theorem rzal 4452
 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 1533   ∈ wcel 2110  ∀wral 3138  ∅c0 4290 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793 This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-sb 2066  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  4454  raaan  4459  raaanv  4460  raaan2  4463  iinrab2  4991  riinrab  5005  reusv2lem2  5299  cnvpo  6137  dffi3  8894  brdom3  9949  dedekind  10802  fimaxre2  11585  mgm0  17865  sgrp0  17907  efgs1  18860  opnnei  21727  axcontlem12  26760  nbgr0edg  27138  prcliscplgr  27195  cplgr0v  27208  0vtxrgr  27357  0vconngr  27971  frgr1v  28049  ubthlem1  28646  rdgssun  34658  matunitlindf  34889  mbfresfi  34937  bddiblnc  34961  blbnd  35064  rrnequiv  35112  upbdrech2  41575  fiminre2  41646  limsupubuz  41994  stoweidlem9  42295  fourierdlem31  42424
 Copyright terms: Public domain W3C validator