Theorem alral 3095

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   ∈ wcel 2147  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ral 3081

This theorem is used by:  falseral0  4473  abnex  7795  find  7931  brdom5  10635  brdom4  10636  hashgt23el  14596  prodeq2w  16108  rpnnen2lem12  16422  umgr2cycllem  30776  umgr2cycl  30777  elpotr  36721  fvineqsnf1  38525  fvineqsneq  38527  phpreu  38719  ordelordALTVD  46040  ssclaxsep  46167  rexrsb  48376