Theorem rnss 5066

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 5010	. . 3 |- ( A C_ B -> `' A C_ `' B )
2		dmss 5037	. . 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 4848	. 2 |- ran A = dom `' A
5		df-rn 4848	. 2 |- ran B = dom `' B
6	3, 4, 5	3sstr4g 3475	1 |- ( A C_ B -> ran A C_ ran B )

Syntax hints:   -> wi 4   C_ wss 3406   `'ccnv 4836   dom cdm 4837   ran crn 4838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-rab 2748  df-v 3049  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-sn 3971  df-pr 3973  df-op 3977  df-br 4406  df-opab 4465  df-cnv 4845  df-dm 4847  df-rn 4848

This theorem is referenced by:  imass1  5206  imass2  5207  ssxpb  5274  ssrnres  5278  sofld  5287  funssxp  5747  fssres  5754  dff2  6039  dff3  6040  fliftf  6213  1stcof  6826  2ndcof  6827  frxp  6911  smores  7076  fodomfi  7855  marypha1lem  7952  marypha1  7953  dfac12lem2  8579  brdom4  8963  smobeth  9016  fpwwe2lem13  9072  nqerf  9360  prdsval  15365  prdsbas  15367  prdsplusg  15368  prdsmulr  15369  prdsvsca  15370  prdshom  15377  catcoppccl  16015  catcfuccl  16016  catcxpccl  16104  lern  16483  odf1o2  17234  gsumzres  17555  gsumzaddlem  17566  gsumzadd  17567  dprdfadd  17665  dprdres  17673  lmss  20326  txss12  20632  txbasval  20633  txkgen  20679  fmss  20973  tsmsxplem1  21179  ustimasn  21255  utopbas  21262  metustexhalf  21583  causs  22280  ovoliunlem1  22467  dvcnvrelem1  22981  taylf  23328  dvlog  23608  perpln2  24768  sspba  26378  imadifxp  28224  metideq  28708  sxbrsigalem5  29122  omsmon  29138  omsmonOLD  29142  carsggect  29162  carsgclctunlem2  29163  nodenselem6  30587  fixssrn  30686  heicant  31987  mblfinlem1  31989  dicval  34756  rntrclfvOAI  35545  diophrw  35613  dnnumch2  35915  lmhmlnmsplit  35957  hbtlem6  36000  mptrcllem  36232  cnvrcl0  36244  rntrcl  36247  dfrcl2  36278  relexpss1d  36309  rp-imass  36378  rnresss  37461  fourierdlem42  38022  fourierdlem42OLD  38023  sge0less  38244  subgrprop3  39358