Theorem rnss 5354

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 5294	. . 3 |- ( A C_ B -> `' A C_ `' B )
2		dmss 5323	. . 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 5125	. 2 |- ran A = dom `' A
5		df-rn 5125	. 2 |- ran B = dom `' B
6	3, 4, 5	3sstr4g 3646	1 |- ( A C_ B -> ran A C_ ran B )

Syntax hints:   -> wi 4   C_ wss 3574   `'ccnv 5113   dom cdm 5114   ran crn 5115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-cnv 5122  df-dm 5124  df-rn 5125

This theorem is referenced by:  imass1  5500  imass2  5501  ssxpb  5568  ssrnres  5572  sofld  5581  funssxp  6061  fssres  6070  dff2  6371  dff3  6372  fliftf  6565  1stcof  7196  2ndcof  7197  frxp  7287  smores  7449  fodomfi  8239  marypha1lem  8339  marypha1  8340  dfac12lem2  8966  brdom4  9352  smobeth  9408  fpwwe2lem13  9464  nqerf  9752  prdsval  16115  prdsbas  16117  prdsplusg  16118  prdsmulr  16119  prdsvsca  16120  prdshom  16127  catcoppccl  16758  catcfuccl  16759  catcxpccl  16847  lern  17225  odf1o2  17988  gsumzres  18310  gsumzaddlem  18321  gsumzadd  18322  dprdfadd  18419  dprdres  18427  lmss  21102  txss12  21408  txbasval  21409  txkgen  21455  fmss  21750  tsmsxplem1  21956  ustimasn  22032  utopbas  22039  metustexhalf  22361  causs  23096  ovoliunlem1  23270  dvcnvrelem1  23780  taylf  24115  dvlog  24397  perpln2  25606  subgrprop3  26168  sspba  27582  imadifxp  29414  metideq  29936  sxbrsigalem5  30350  omsmon  30360  carsggect  30380  carsgclctunlem2  30381  fixssrn  32014  heicant  33444  mblfinlem1  33446  dicval  36465  rntrclfvOAI  37254  diophrw  37322  dnnumch2  37615  lmhmlnmsplit  37657  hbtlem6  37699  mptrcllem  37920  cnvrcl0  37932  rntrcl  37935  dfrcl2  37966  relexpss1d  37997  rp-imass  38065  rfovcnvf1od  38298  rnresss  39365  supcnvlimsup  39972  fourierdlem42  40366  sge0less  40609