Theorem ssralv 3220

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

Syntax hints:   -> wi 4   e. wcel 2148   A.wral 2455   C_ wss 3130

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-ral 2460  df-in 3136  df-ss 3143

This theorem is referenced by:  iinss1  3899  poss  4299  sess2  4339  trssord  4381  funco  5257  funimaexglem  5300  isores3  5816  isoini2  5820  smores  6293  smores2  6295  tfrlem5  6315  resixp  6733  ac6sfi  6898  difinfinf  7100  peano5nnnn  7891  peano5nni  8922  caucvgre  10990  rexanuz  10997  cau3lem  11123  isumclim3  11431  fsumiun  11485  pcfac  12348  ctinf  12431  strsetsid  12495  imasaddfnlemg  12735  tgcn  13711  tgcnp  13712  cnss2  13730  cncnp  13733  sslm  13750  metrest  14009  rescncf  14071  suplociccex  14106  limcresi  14138  nninfsellemeq  14766