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  3885  poss  4283  sess2  4323  trssord  4365  funco  5238  funimaexglem  5281  isores3  5794  isoini2  5798  smores  6271  smores2  6273  tfrlem5  6293  resixp  6711  ac6sfi  6876  difinfinf  7078  peano5nnnn  7854  peano5nni  8881  caucvgre  10945  rexanuz  10952  cau3lem  11078  isumclim3  11386  fsumiun  11440  pcfac  12302  ctinf  12385  strsetsid  12449  tgcn  13002  tgcnp  13003  cnss2  13021  cncnp  13024  sslm  13041  metrest  13300  rescncf  13362  suplociccex  13397  limcresi  13429  nninfsellemeq  14047