Theorem alral 3065

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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2108  ∀wral 3051

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 3052

This theorem is referenced by:  abnex  7751  find  7891  brdom5  10543  brdom4  10544  hashgt23el  14442  prodeq2w  15926  rpnnen2lem12  16243  umgr2cycllem  35162  umgr2cycl  35163  elpotr  35799  fvineqsnf1  37428  fvineqsneq  37430  phpreu  37628  ordelordALTVD  44891  ssclaxsep  45007  rexrsb  47129