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

Theorem alral 3076
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 3063 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
31, 2sylibr 233 1 (∀𝑥𝜑 → ∀𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1540  wcel 2107  wral 3062
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 3063
This theorem is referenced by:  abnex  7744  find  7887  findOLD  7888  brdom5  10524  brdom4  10525  hashgt23el  14384  prodeq2w  15856  rpnnen2lem12  16168  umgr2cycllem  34131  umgr2cycl  34132  elpotr  34753  fvineqsnf1  36291  fvineqsneq  36293  phpreu  36472  ordelordALTVD  43628  rexrsb  45808
  Copyright terms: Public domain W3C validator