Theorem ssralv 3256

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

Syntax hints:   → wi 4   ∈ wcel 2175  ∀wral 2483   ⊆ wss 3165

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-ral 2488  df-in 3171  df-ss 3178

This theorem is referenced by:  iinss1  3938  poss  4344  sess2  4384  trssord  4426  funco  5310  funimaexglem  5356  isores3  5883  isoini2  5887  smores  6377  smores2  6379  tfrlem5  6399  resixp  6819  ac6sfi  6994  difinfinf  7202  peano5nnnn  8004  peano5nni  9038  caucvgre  11234  rexanuz  11241  cau3lem  11367  isumclim3  11676  fsumiun  11730  pcfac  12615  ctinf  12743  strsetsid  12807  imasaddfnlemg  13088  tgcn  14622  tgcnp  14623  cnss2  14641  cncnp  14644  sslm  14661  metrest  14920  rescncf  14995  suplociccex  15039  limcresi  15080  nninfsellemeq  15884