Theorem ssralv 3288

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

Syntax hints:   → wi 4   ∈ wcel 2200  ∀wral 2508   ⊆ wss 3197

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-ral 2513  df-in 3203  df-ss 3210

This theorem is referenced by:  iinss1  3977  poss  4389  sess2  4429  trssord  4471  funco  5358  funimaexglem  5404  isores3  5945  isoini2  5949  smores  6444  smores2  6446  tfrlem5  6466  resixp  6888  ac6sfi  7068  difinfinf  7279  peano5nnnn  8090  peano5nni  9124  caucvgre  11507  rexanuz  11514  cau3lem  11640  isumclim3  11949  fsumiun  12003  pcfac  12888  ctinf  13016  strsetsid  13080  imasaddfnlemg  13362  tgcn  14897  tgcnp  14898  cnss2  14916  cncnp  14919  sslm  14936  metrest  15195  rescncf  15270  suplociccex  15314  limcresi  15355  uspgr2wlkeq  16106  nninfsellemeq  16440