Theorem ssralv 3248

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

Syntax hints:   → wi 4   ∈ wcel 2167  ∀wral 2475   ⊆ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-ral 2480  df-in 3163  df-ss 3170

This theorem is referenced by:  iinss1  3929  poss  4334  sess2  4374  trssord  4416  funco  5299  funimaexglem  5342  isores3  5865  isoini2  5869  smores  6359  smores2  6361  tfrlem5  6381  resixp  6801  ac6sfi  6968  difinfinf  7176  peano5nnnn  7976  peano5nni  9010  caucvgre  11163  rexanuz  11170  cau3lem  11296  isumclim3  11605  fsumiun  11659  pcfac  12544  ctinf  12672  strsetsid  12736  imasaddfnlemg  13016  tgcn  14528  tgcnp  14529  cnss2  14547  cncnp  14550  sslm  14567  metrest  14826  rescncf  14901  suplociccex  14945  limcresi  14986  nninfsellemeq  15745