Theorem alral 3094

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

Syntax hints:   → wi 4  ∀wal 1568   ∈ wcel 2143  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839

This theorem depends on definitions:  df-bi 210  df-ral 3080

This theorem is referenced by:  falseral0  4476  abnex  7757  find  7893  brdom5  10514  brdom4  10515  hashgt23el  14463  prodeq2w  15966  rpnnen2lem12  16282  umgr2cycllem  35610  umgr2cycl  35611  elpotr  36249  fvineqsnf1  38034  fvineqsneq  38036  phpreu  38233  ordelordALTVD  45555  ssclaxsep  45671  rexrsb  47814