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

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

Proof of Theorem alral
StepHypRef Expression
1 ala1 1810 . 2 (∀𝑥𝜑 → ∀𝑥(𝑥𝐴𝜑))
2 df-ral 3060 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
31, 2sylibr 234 1 (∀𝑥𝜑 → ∀𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1535  wcel 2106  wral 3059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806
This theorem depends on definitions:  df-bi 207  df-ral 3060
This theorem is referenced by:  abnex  7776  find  7918  brdom5  10567  brdom4  10568  hashgt23el  14460  prodeq2w  15943  rpnnen2lem12  16258  umgr2cycllem  35125  umgr2cycl  35126  elpotr  35763  fvineqsnf1  37393  fvineqsneq  37395  phpreu  37591  ordelordALTVD  44865  ssclaxsep  44947  rexrsb  47050
  Copyright terms: Public domain W3C validator