Theorem alral 3097

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

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

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 3083

This theorem is used by:  falseral0  4480  abnex  7765  find  7901  brdom5  10531  brdom4  10532  hashgt23el  14481  prodeq2w  15990  rpnnen2lem12  16306  umgr2cycllem  35652  umgr2cycl  35653  elpotr  36291  fvineqsnf1  38096  fvineqsneq  38098  phpreu  38295  ordelordALTVD  45615  ssclaxsep  45731  rexrsb  47877