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

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

Proof of Theorem alral
StepHypRef Expression
1 ala1 1815 . 2 (∀𝑥𝜑 → ∀𝑥(𝑥𝐴𝜑))
2 df-ral 3075 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
31, 2sylibr 237 1 (∀𝑥𝜑 → ∀𝑥𝐴 𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1536   ∈ wcel 2111  ∀wral 3070 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811 This theorem depends on definitions:  df-bi 210  df-ral 3075 This theorem is referenced by:  abnex  7483  find  7611  findOLD  7612  brdom5  9994  brdom4  9995  hashgt23el  13840  prodeq2w  15319  rpnnen2lem12  15631  umgr2cycllem  32622  umgr2cycl  32623  elpotr  33277  fvineqsnf1  35133  fvineqsneq  35135  phpreu  35347  ordelordALTVD  41974  rexrsb  44051
 Copyright terms: Public domain W3C validator