Theorem alral 3075

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 1815	. 2 ⊢ (∀𝑥𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		df-ral 3062	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
3	1, 2	sylibr 233	1 ⊢ (∀𝑥𝜑 → ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2106  ∀wral 3061

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

This theorem depends on definitions:  df-bi 206  df-ral 3062

This theorem is referenced by:  abnex  7740  find  7883  findOLD  7884  brdom5  10520  brdom4  10521  hashgt23el  14380  prodeq2w  15852  rpnnen2lem12  16164  umgr2cycllem  34119  umgr2cycl  34120  elpotr  34741  fvineqsnf1  36279  fvineqsneq  36281  phpreu  36460  ordelordALTVD  43613  rexrsb  45794