Theorem alral 3067

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 1815	. 2 ⊢ (∀𝑥𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2	1	ralrid 3060	1 ⊢ (∀𝑥𝜑 → ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2114  ∀wral 3052

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 207  df-ral 3053

This theorem is referenced by:  falseral0  4469  abnex  7712  find  7847  brdom5  10451  brdom4  10452  hashgt23el  14359  prodeq2w  15845  rpnnen2lem12  16162  umgr2cycllem  35353  umgr2cycl  35354  elpotr  35992  fvineqsnf1  37659  fvineqsneq  37661  phpreu  37849  ordelordALTVD  45216  ssclaxsep  45332  rexrsb  47454