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

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

Proof of Theorem alral
StepHypRef Expression
1 ala1 1807 . 2 (∀𝑥𝜑 → ∀𝑥(𝑥𝐴𝜑))
2 df-ral 3051 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
31, 2sylibr 233 1 (∀𝑥𝜑 → ∀𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1531  wcel 2098  wral 3050
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803
This theorem depends on definitions:  df-bi 206  df-ral 3051
This theorem is referenced by:  abnex  7760  find  7903  brdom5  10554  brdom4  10555  hashgt23el  14419  prodeq2w  15892  rpnnen2lem12  16205  umgr2cycllem  34881  umgr2cycl  34882  elpotr  35508  fvineqsnf1  37020  fvineqsneq  37022  phpreu  37208  ordelordALTVD  44448  rexrsb  46618
  Copyright terms: Public domain W3C validator