Theorem alral 3069

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

Syntax hints:   → wi 4  ∀wal 1545   ∈ wcel 2119  ∀wral 3054

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

This theorem depends on definitions:  df-bi 208  df-ral 3055

This theorem is referenced by:  falseral0  4449  abnex  7707  find  7842  brdom5  10449  brdom4  10450  hashgt23el  14384  prodeq2w  15873  rpnnen2lem12  16190  umgr2cycllem  35375  umgr2cycl  35376  elpotr  36014  fvineqsnf1  37779  fvineqsneq  37781  phpreu  37978  ordelordALTVD  45317  ssclaxsep  45433  rexrsb  47570