Theorem ssralv 3288

Description: Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006.)

Assertion

Ref	Expression
ssralv	|- ( A C_ B -> ( A. x e. B ph -> A. x e. A ph ) )

Distinct variable groups:   x, A   x, B

Allowed substitution hint:   ph( x)

Proof of Theorem ssralv

Step	Hyp	Ref	Expression
1		ssel 3218	. . 3 |- ( A C_ B -> ( x e. A -> x e. B ) )
2	1	imim1d 75	. 2 |- ( A C_ B -> ( ( x e. B -> ph ) -> ( x e. A -> ph ) ) )
3	2	ralimdv2 2600	1 |- ( A C_ B -> ( A. x e. B ph -> A. x e. A ph ) )

Syntax hints:   -> wi 4   e. wcel 2200   A.wral 2508   C_ 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  3977  poss  4389  sess2  4429  trssord  4471  funco  5358  funimaexglem  5404  isores3  5939  isoini2  5943  smores  6438  smores2  6440  tfrlem5  6460  resixp  6880  ac6sfi  7060  difinfinf  7268  peano5nnnn  8079  peano5nni  9113  caucvgre  11492  rexanuz  11499  cau3lem  11625  isumclim3  11934  fsumiun  11988  pcfac  12873  ctinf  13001  strsetsid  13065  imasaddfnlemg  13347  tgcn  14882  tgcnp  14883  cnss2  14901  cncnp  14904  sslm  14921  metrest  15180  rescncf  15255  suplociccex  15299  limcresi  15340  uspgr2wlkeq  16076  nninfsellemeq  16380