Theorem ssralv 3288

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

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

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 3203  df-ss 3210

This theorem is referenced by:  iinss1  3976  poss  4388  sess2  4428  trssord  4470  funco  5357  funimaexglem  5403  isores3  5938  isoini2  5942  smores  6436  smores2  6438  tfrlem5  6458  resixp  6878  ac6sfi  7056  difinfinf  7264  peano5nnnn  8075  peano5nni  9109  caucvgre  11487  rexanuz  11494  cau3lem  11620  isumclim3  11929  fsumiun  11983  pcfac  12868  ctinf  12996  strsetsid  13060  imasaddfnlemg  13342  tgcn  14876  tgcnp  14877  cnss2  14895  cncnp  14898  sslm  14915  metrest  15174  rescncf  15249  suplociccex  15293  limcresi  15334  nninfsellemeq  16339