Theorem ssralv 3156

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

Syntax hints:   -> wi 4   e. wcel 1480   A.wral 2414   C_ wss 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-ral 2419  df-in 3072  df-ss 3079

This theorem is referenced by:  iinss1  3820  poss  4215  sess2  4255  trssord  4297  funco  5158  funimaexglem  5201  isores3  5709  isoini2  5713  smores  6182  smores2  6184  tfrlem5  6204  resixp  6620  ac6sfi  6785  difinfinf  6979  peano5nnnn  7693  peano5nni  8716  caucvgre  10746  rexanuz  10753  cau3lem  10879  isumclim3  11185  fsumiun  11239  ctinf  11932  strsetsid  11981  tgcn  12366  tgcnp  12367  cnss2  12385  cncnp  12388  sslm  12405  metrest  12664  rescncf  12726  suplociccex  12761  limcresi  12793  nninfsellemeq  13199