Theorem alral 3090

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

Syntax hints:   → wi 4  ∀wal 1557   ∈ wcel 2141  ∀wral 3075

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

This theorem depends on definitions:  df-bi 209  df-ral 3076

This theorem is referenced by:  falseral0  4467  abnex  7736  find  7872  brdom5  10483  brdom4  10484  hashgt23el  14434  prodeq2w  15923  rpnnen2lem12  16240  umgr2cycllem  35454  umgr2cycl  35455  elpotr  36093  fvineqsnf1  37868  fvineqsneq  37870  phpreu  38067  ordelordALTVD  45406  ssclaxsep  45522  rexrsb  47658