Theorem rnss 5221

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 5165	. . 3 |- ( A C_ B -> `' A C_ `' B )
2		dmss 5192	. . 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 5000	. 2 |- ran A = dom `' A
5		df-rn 5000	. 2 |- ran B = dom `' B
6	3, 4, 5	3sstr4g 3530	1 |- ( A C_ B -> ran A C_ ran B )

Syntax hints:   -> wi 4   C_ wss 3461   `'ccnv 4988   dom cdm 4989   ran crn 4990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438  df-opab 4496  df-cnv 4997  df-dm 4999  df-rn 5000

This theorem is referenced by:  imass1  5361  imass2  5362  ssxpb  5431  ssrnres  5435  sofld  5445  funssxp  5734  fssres  5741  dff2  6028  dff3  6029  fliftf  6198  1stcof  6813  2ndcof  6814  frxp  6895  smores  7025  fodomfi  7801  marypha1lem  7895  marypha1  7896  dfac12lem2  8527  brdom4  8911  smobeth  8964  fpwwe2lem13  9023  nqerf  9311  prdsval  14834  prdsbas  14836  prdsplusg  14837  prdsmulr  14838  prdsvsca  14839  prdshom  14846  catcoppccl  15414  catcfuccl  15415  catcxpccl  15455  lern  15834  odf1o2  16572  gsumzres  16893  gsumzresOLD  16897  gsumzaddlem  16913  gsumzadd  16914  gsumzaddlemOLD  16915  gsumzaddOLD  16916  dprdfadd  17039  dprdfaddOLD  17046  dprdres  17054  lmss  19777  txss12  20084  txbasval  20085  txkgen  20131  fmss  20425  tsmsxplem1  20633  ustimasn  20709  utopbas  20716  metustexhalfOLD  21044  metustexhalf  21045  causs  21715  ovoliunlem1  21891  dvcnvrelem1  22396  taylf  22734  dvlog  23010  perpln2  24066  sspba  25618  imadifxp  27436  metideq  27850  sxbrsigalem5  28237  omsmon  28245  nodenselem6  29422  fixssrn  29533  heicant  30025  mblfinlem1  30027  diophrw  30668  dnnumch2  30967  lmhmlnmsplit  31009  hbtlem6  31054  fourierdlem42  31885  dicval  36778  rp-imass  37617