Theorem ssralv 3289

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

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

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 3204  df-ss 3211

This theorem is referenced by:  iinss1  3980  poss  4393  sess2  4433  trssord  4475  funco  5364  funimaexglem  5410  isores3  5951  isoini2  5955  smores  6453  smores2  6455  tfrlem5  6475  resixp  6897  ac6sfi  7080  difinfinf  7291  peano5nnnn  8102  peano5nni  9136  caucvgre  11532  rexanuz  11539  cau3lem  11665  isumclim3  11974  fsumiun  12028  pcfac  12913  ctinf  13041  strsetsid  13105  imasaddfnlemg  13387  tgcn  14922  tgcnp  14923  cnss2  14941  cncnp  14944  sslm  14961  metrest  15220  rescncf  15295  suplociccex  15339  limcresi  15380  uspgr2wlkeq  16162  nninfsellemeq  16552