Theorem ssralv 3211

Description: Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006.)

Assertion

Ref	Expression
ssralv	⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ssralv

Step	Hyp	Ref	Expression
1		ssel 3141	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	imim1d 75	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑)))
3	2	ralimdv2 2540	1 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))

Syntax hints:   → wi 4   ∈ wcel 2141  ∀wral 2448   ⊆ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-ral 2453  df-in 3127  df-ss 3134

This theorem is referenced by:  iinss1  3883  poss  4281  sess2  4321  trssord  4363  funco  5236  funimaexglem  5279  isores3  5791  isoini2  5795  smores  6268  smores2  6270  tfrlem5  6290  resixp  6707  ac6sfi  6872  difinfinf  7074  peano5nnnn  7841  peano5nni  8868  caucvgre  10932  rexanuz  10939  cau3lem  11065  isumclim3  11373  fsumiun  11427  pcfac  12289  ctinf  12372  strsetsid  12436  tgcn  12961  tgcnp  12962  cnss2  12980  cncnp  12983  sslm  13000  metrest  13259  rescncf  13321  suplociccex  13356  limcresi  13388  nninfsellemeq  14007