Theorem alral 3080

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

Syntax hints:   → wi 4  ∀wal 1537   ∈ wcel 2106  ∀wral 3064

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

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

This theorem is referenced by:  abnex  7607  find  7743  findOLD  7744  brdom5  10285  brdom4  10286  hashgt23el  14139  prodeq2w  15622  rpnnen2lem12  15934  umgr2cycllem  33102  umgr2cycl  33103  elpotr  33757  fvineqsnf1  35581  fvineqsneq  35583  phpreu  35761  ordelordALTVD  42487  rexrsb  44592