Theorem ssralv 3206

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 3136	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	imim1d 75	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑)))
3	2	ralimdv2 2536	1 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))

Syntax hints:   → wi 4   ∈ wcel 2136  ∀wral 2444   ⊆ wss 3116

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-ral 2449  df-in 3122  df-ss 3129

This theorem is referenced by:  iinss1  3878  poss  4276  sess2  4316  trssord  4358  funco  5228  funimaexglem  5271  isores3  5783  isoini2  5787  smores  6260  smores2  6262  tfrlem5  6282  resixp  6699  ac6sfi  6864  difinfinf  7066  peano5nnnn  7833  peano5nni  8860  caucvgre  10923  rexanuz  10930  cau3lem  11056  isumclim3  11364  fsumiun  11418  pcfac  12280  ctinf  12363  strsetsid  12427  tgcn  12848  tgcnp  12849  cnss2  12867  cncnp  12870  sslm  12887  metrest  13146  rescncf  13208  suplociccex  13243  limcresi  13275  nninfsellemeq  13894