Theorem alral 3061

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

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2111  ∀wral 3047

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

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

This theorem is referenced by:  abnex  7690  find  7825  brdom5  10417  brdom4  10418  hashgt23el  14328  prodeq2w  15814  rpnnen2lem12  16131  umgr2cycllem  35172  umgr2cycl  35173  elpotr  35814  fvineqsnf1  37443  fvineqsneq  37445  phpreu  37643  ordelordALTVD  44898  ssclaxsep  45014  rexrsb  47130