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  4343  sess2  4383  trssord  4425  funco  5308  funimaexglem  5351  isores3  5874  isoini2  5878  smores  6368  smores2  6370  tfrlem5  6390  resixp  6810  ac6sfi  6977  difinfinf  7185  peano5nnnn  7987  peano5nni  9021  caucvgre  11211  rexanuz  11218  cau3lem  11344  isumclim3  11653  fsumiun  11707  pcfac  12592  ctinf  12720  strsetsid  12784  imasaddfnlemg  13064  tgcn  14598  tgcnp  14599  cnss2  14617  cncnp  14620  sslm  14637  metrest  14896  rescncf  14971  suplociccex  15015  limcresi  15056  nninfsellemeq  15815