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  35653  umgr2cycl  35654  elpotr  36292  fvineqsnf1  38097  fvineqsneq  38099  phpreu  38296  ordelordALTVD  45616  ssclaxsep  45732  rexrsb  47878