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  5945  isoini2  5949  smores  6444  smores2  6446  tfrlem5  6466  resixp  6888  ac6sfi  7068  difinfinf  7279  peano5nnnn  8090  peano5nni  9124  caucvgre  11508  rexanuz  11515  cau3lem  11641  isumclim3  11950  fsumiun  12004  pcfac  12889  ctinf  13017  strsetsid  13081  imasaddfnlemg  13363  tgcn  14898  tgcnp  14899  cnss2  14917  cncnp  14920  sslm  14937  metrest  15196  rescncf  15271  suplociccex  15315  limcresi  15356  uspgr2wlkeq  16111  nninfsellemeq  16468