Theorem alral 3067

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	1	ralrid 3060	1 ⊢ (∀𝑥𝜑 → ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2114  ∀wral 3052

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 207  df-ral 3053

This theorem is referenced by:  falseral0  4455  abnex  7704  find  7839  brdom5  10442  brdom4  10443  hashgt23el  14377  prodeq2w  15866  rpnnen2lem12  16183  umgr2cycllem  35338  umgr2cycl  35339  elpotr  35977  fvineqsnf1  37740  fvineqsneq  37742  phpreu  37939  ordelordALTVD  45311  ssclaxsep  45427  rexrsb  47560