Theorem ssralv 3257

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 3187	. . 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 2576	1 |- ( A C_ B -> ( A. x e. B ph -> A. x e. A ph ) )

Syntax hints:   -> wi 4   e. wcel 2176   A.wral 2484   C_ wss 3166

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-ral 2489  df-in 3172  df-ss 3179

This theorem is referenced by:  iinss1  3939  poss  4346  sess2  4386  trssord  4428  funco  5312  funimaexglem  5358  isores3  5886  isoini2  5890  smores  6380  smores2  6382  tfrlem5  6402  resixp  6822  ac6sfi  6997  difinfinf  7205  peano5nnnn  8007  peano5nni  9041  caucvgre  11325  rexanuz  11332  cau3lem  11458  isumclim3  11767  fsumiun  11821  pcfac  12706  ctinf  12834  strsetsid  12898  imasaddfnlemg  13179  tgcn  14713  tgcnp  14714  cnss2  14732  cncnp  14735  sslm  14752  metrest  15011  rescncf  15086  suplociccex  15130  limcresi  15171  nninfsellemeq  15988