Theorem alral 3059

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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2109  ∀wral 3045

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

This theorem depends on definitions:  df-bi 207  df-ral 3046

This theorem is referenced by:  abnex  7736  find  7874  brdom5  10489  brdom4  10490  hashgt23el  14396  prodeq2w  15883  rpnnen2lem12  16200  umgr2cycllem  35134  umgr2cycl  35135  elpotr  35776  fvineqsnf1  37405  fvineqsneq  37407  phpreu  37605  ordelordALTVD  44863  ssclaxsep  44979  rexrsb  47105