Theorem alral 3066

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 3059	1 ⊢ (∀𝑥𝜑 → ∀𝑥 ∈ 𝐴 𝜑)

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

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 3052

This theorem is referenced by:  falseral0  4454  abnex  7711  find  7846  brdom5  10451  brdom4  10452  hashgt23el  14386  prodeq2w  15875  rpnnen2lem12  16192  umgr2cycllem  35322  umgr2cycl  35323  elpotr  35961  fvineqsnf1  37726  fvineqsneq  37728  phpreu  37925  ordelordALTVD  45293  ssclaxsep  45409  rexrsb  47548