Theorem alral 3094

Description: Universal quantification implies restricted quantification. (Contributed by NM, 20-Oct-2006.)

Assertion

Ref	Expression
alral	⊢ (∀𝑥𝜑 → ∀𝑥 ∈ 𝐴 𝜑)

Proof of Theorem alral

Step	Hyp	Ref	Expression
1		ala1 1836	. 2 ⊢ (∀𝑥𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2	1	ralrid 3087	1 ⊢ (∀𝑥𝜑 → ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4  ∀wal 1561   ∈ wcel 2145  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832

This theorem depends on definitions:  df-bi 210  df-ral 3080

This theorem is referenced by:  falseral0  4471  abnex  7744  find  7880  brdom5  10501  brdom4  10502  hashgt23el  14451  prodeq2w  15954  rpnnen2lem12  16271  umgr2cycllem  35503  umgr2cycl  35504  elpotr  36142  fvineqsnf1  37916  fvineqsneq  37918  phpreu  38115  ordelordALTVD  45440  ssclaxsep  45556  rexrsb  47692