Theorem rnss 5229

Description: Subset theorem for range. (Contributed by NM, 22-Mar-1998.)

Assertion

Ref	Expression
rnss	|- ( A C_ B -> ran A C_ ran B )

Proof of Theorem rnss

Step	Hyp	Ref	Expression
1		cnvss 5173	. . 3 |- ( A C_ B -> `' A C_ `' B )
2		dmss 5200	. . 3 |- ( `' A C_ `' B -> dom `' A C_ dom `' B )
3	1, 2	syl 16	. 2 |- ( A C_ B -> dom `' A C_ dom `' B )
4		df-rn 5010	. 2 |- ran A = dom `' A
5		df-rn 5010	. 2 |- ran B = dom `' B
6	3, 4, 5	3sstr4g 3545	1 |- ( A C_ B -> ran A C_ ran B )

Syntax hints:   -> wi 4   C_ wss 3476   `'ccnv 4998   dom cdm 4999   ran crn 5000

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-opab 4506  df-cnv 5007  df-dm 5009  df-rn 5010

This theorem is referenced by:  imass1  5369  imass2  5370  ssxpb  5439  ssrnres  5443  sofld  5453  funssxp  5742  fssres  5749  dff2  6031  dff3  6032  fliftf  6199  1stcof  6809  2ndcof  6810  frxp  6890  smores  7020  fodomfi  7795  marypha1lem  7889  marypha1  7890  dfac12lem2  8520  brdom4  8904  smobeth  8957  fpwwe2lem13  9016  nqerf  9304  prdsval  14706  prdsbas  14708  prdsplusg  14709  prdsmulr  14710  prdsvsca  14711  prdshom  14718  catcoppccl  15289  catcfuccl  15290  catcxpccl  15330  lern  15708  odf1o2  16389  gsumzres  16705  gsumzresOLD  16709  gsumzaddlem  16725  gsumzadd  16726  gsumzaddlemOLD  16727  gsumzaddOLD  16728  dprdfadd  16850  dprdfaddOLD  16857  dprdres  16865  cnrest  19552  lmss  19565  txss12  19841  txbasval  19842  txkgen  19888  fmss  20182  tsmsxplem1  20390  ustimasn  20466  utopbas  20473  metustexhalfOLD  20801  metustexhalf  20802  causs  21472  ovoliunlem1  21648  dvcnvrelem1  22153  taylf  22490  dvlog  22760  perpln2  23796  sspba  25316  imadifxp  27131  metideq  27508  sxbrsigalem5  27899  omsmon  27907  nodenselem6  29023  fixssrn  29134  heicant  29626  mblfinlem1  29628  diophrw  30296  dnnumch2  30595  lmhmlnmsplit  30637  hbtlem6  30682  fourierdlem42  31449  dicval  35973  rp-imass  36796