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 1813 . 2 (∀𝑥𝜑 → ∀𝑥(𝑥𝐴𝜑))
2 df-ral 3062 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
31, 2sylibr 234 1 (∀𝑥𝜑 → ∀𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1538  wcel 2108  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 207  df-ral 3062
This theorem is referenced by:  abnex  7777  find  7917  brdom5  10569  brdom4  10570  hashgt23el  14463  prodeq2w  15946  rpnnen2lem12  16261  umgr2cycllem  35145  umgr2cycl  35146  elpotr  35782  fvineqsnf1  37411  fvineqsneq  37413  phpreu  37611  ordelordALTVD  44887  ssclaxsep  44999  rexrsb  47112
  Copyright terms: Public domain W3C validator