Theorem alral 3093

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

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

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 3079

This theorem is used by:  falseral0  4473  abnex  7760  find  7896  brdom5  10536  brdom4  10537  hashgt23el  14493  prodeq2w  16003  rpnnen2lem12  16319  umgr2cycllem  30633  umgr2cycl  30634  elpotr  36366  fvineqsnf1  38172  fvineqsneq  38174  phpreu  38366  ordelordALTVD  45697  ssclaxsep  45813  rexrsb  47996