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  7978  peano5nni  9012  caucvgre  11165  rexanuz  11172  cau3lem  11298  isumclim3  11607  fsumiun  11661  pcfac  12546  ctinf  12674  strsetsid  12738  imasaddfnlemg  13018  tgcn  14552  tgcnp  14553  cnss2  14571  cncnp  14574  sslm  14591  metrest  14850  rescncf  14925  suplociccex  14969  limcresi  15010  nninfsellemeq  15769