Theorem rnss 5068

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 5012	. . 3 |- ( A C_ B -> `' A C_ `' B )
2		dmss 5039	. . 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 4851	. 2 |- ran A = dom `' A
5		df-rn 4851	. 2 |- ran B = dom `' B
6	3, 4, 5	3sstr4g 3397	1 |- ( A C_ B -> ran A C_ ran B )

Syntax hints:   -> wi 4   C_ wss 3328   `'ccnv 4839   dom cdm 4840   ran crn 4841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-br 4293  df-opab 4351  df-cnv 4848  df-dm 4850  df-rn 4851

This theorem is referenced by:  imass1  5203  imass2  5204  ssxpb  5272  ssrnres  5276  sofld  5286  funssxp  5571  fssres  5578  dff2  5855  dff3  5856  fliftf  6008  1stcof  6604  2ndcof  6605  frxp  6682  smores  6813  fodomfi  7590  marypha1lem  7683  marypha1  7684  dfac12lem2  8313  brdom4  8697  smobeth  8750  fpwwe2lem13  8809  nqerf  9099  prdsval  14393  prdsbas  14395  prdsplusg  14396  prdsmulr  14397  prdsvsca  14398  prdshom  14405  catcoppccl  14976  catcfuccl  14977  catcxpccl  15017  lern  15395  odf1o2  16072  gsumzres  16388  gsumzresOLD  16392  gsumzaddlem  16408  gsumzadd  16409  gsumzaddlemOLD  16410  gsumzaddOLD  16411  dprdfadd  16510  dprdfaddOLD  16517  dprdres  16525  cnrest  18889  lmss  18902  txss12  19178  txbasval  19179  txkgen  19225  fmss  19519  tsmsxplem1  19727  ustimasn  19803  utopbas  19810  metustexhalfOLD  20138  metustexhalf  20139  causs  20809  ovoliunlem1  20985  dvcnvrelem1  21489  taylf  21826  dvlog  22096  sspba  24125  imadifxp  25939  metideq  26320  sxbrsigalem5  26703  omsmon  26711  nodenselem6  27827  fixssrn  27938  heicant  28426  mblfinlem1  28428  diophrw  29097  dnnumch2  29398  lmhmlnmsplit  29440  hbtlem6  29485  dicval  34821