Theorem alral 3091

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1567   ∈ wcel 2144  ∀wral 3076

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

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

This theorem is used by:  falseral0  4469  abnex  7771  find  7907  brdom5  10611  brdom4  10612  hashgt23el  14572  prodeq2w  16084  rpnnen2lem12  16398  umgr2cycllem  30751  umgr2cycl  30752  elpotr  36635  fvineqsnf1  38426  fvineqsneq  38428  phpreu  38620  ordelordALTVD  45942  ssclaxsep  46065  rexrsb  48263