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

Theorem alral 3075
Description: Universal quantification implies restricted quantification. (Contributed by NM, 20-Oct-2006.)
Assertion
Ref Expression
alral (∀𝑥𝜑 → ∀𝑥𝐴 𝜑)

Proof of Theorem alral
StepHypRef Expression
1 ala1 1816 . 2 (∀𝑥𝜑 → ∀𝑥(𝑥𝐴𝜑))
2 df-ral 3062 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
31, 2sylibr 233 1 (∀𝑥𝜑 → ∀𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1540  wcel 2107  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812
This theorem depends on definitions:  df-bi 206  df-ral 3062
This theorem is referenced by:  abnex  7692  find  7834  findOLD  7835  brdom5  10470  brdom4  10471  hashgt23el  14330  prodeq2w  15800  rpnnen2lem12  16112  umgr2cycllem  33791  umgr2cycl  33792  elpotr  34412  fvineqsnf1  35927  fvineqsneq  35929  phpreu  36108  ordelordALTVD  43237  rexrsb  45418
  Copyright terms: Public domain W3C validator