Theorem rnss 5069

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 17	. 2 |- ( A C_ B -> dom `' A C_ dom `' B )
4		df-rn 4850	. 2 |- ran A = dom `' A
5		df-rn 4850	. 2 |- ran B = dom `' B
6	3, 4, 5	3sstr4g 3459	1 |- ( A C_ B -> ran A C_ ran B )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-br 4396  df-opab 4455  df-cnv 4847  df-dm 4849  df-rn 4850

This theorem is referenced by:  imass1  5209  imass2  5210  ssxpb  5277  ssrnres  5281  sofld  5290  funssxp  5754  fssres  5761  dff2  6049  dff3  6050  fliftf  6226  1stcof  6840  2ndcof  6841  frxp  6925  smores  7089  fodomfi  7868  marypha1lem  7965  marypha1  7966  dfac12lem2  8592  brdom4  8976  smobeth  9029  fpwwe2lem13  9085  nqerf  9373  prdsval  15431  prdsbas  15433  prdsplusg  15434  prdsmulr  15435  prdsvsca  15436  prdshom  15443  catcoppccl  16081  catcfuccl  16082  catcxpccl  16170  lern  16549  odf1o2  17300  gsumzres  17621  gsumzaddlem  17632  gsumzadd  17633  dprdfadd  17731  dprdres  17739  lmss  20391  txss12  20697  txbasval  20698  txkgen  20744  fmss  21039  tsmsxplem1  21245  ustimasn  21321  utopbas  21328  metustexhalf  21649  causs  22346  ovoliunlem1  22533  dvcnvrelem1  23048  taylf  23395  dvlog  23675  perpln2  24835  sspba  26447  imadifxp  28288  metideq  28770  sxbrsigalem5  29183  omsmon  29199  omsmonOLD  29203  carsggect  29223  carsgclctunlem2  29224  nodenselem6  30646  fixssrn  30745  heicant  32039  mblfinlem1  32041  dicval  34815  rntrclfvOAI  35604  diophrw  35672  dnnumch2  35974  lmhmlnmsplit  36016  hbtlem6  36059  mptrcllem  36291  cnvrcl0  36303  rntrcl  36306  dfrcl2  36337  relexpss1d  36368  rp-imass  36437  rnresss  37522  fourierdlem42  38124  fourierdlem42OLD  38125  sge0less  38348  subgrprop3  39512