Theorem alral 3092

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 1846	. 2 ⊢ (∀𝑥𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2	1	ralrid 3085	1 ⊢ (∀𝑥𝜑 → ∀𝑥 ∈ 𝐴 𝜑)

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   ∈ wcel 2145  ∀wral 3077

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ral 3078

This theorem is used by:  falseral0  4470  abnex  7760  find  7896  brdom5  10589  brdom4  10590  hashgt23el  14549  prodeq2w  16059  rpnnen2lem12  16373  umgr2cycllem  30728  umgr2cycl  30729  elpotr  36513  fvineqsnf1  38301  fvineqsneq  38303  phpreu  38495  ordelordALTVD  45808  ssclaxsep  45924  rexrsb  48114