Theorem rnss 5157

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 5101	. . 3 |- ( A C_ B -> `' A C_ `' B )
2		dmss 5128	. . 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 4937	. 2 |- ran A = dom `' A
5		df-rn 4937	. 2 |- ran B = dom `' B
6	3, 4, 5	3sstr4g 3471	1 |- ( A C_ B -> ran A C_ ran B )

Syntax hints:   -> wi 4   C_ wss 3402   `'ccnv 4925   dom cdm 4926   ran crn 4927

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-rab 2751  df-v 3049  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-nul 3725  df-if 3871  df-sn 3958  df-pr 3960  df-op 3964  df-br 4381  df-opab 4439  df-cnv 4934  df-dm 4936  df-rn 4937

This theorem is referenced by:  imass1  5296  imass2  5297  ssxpb  5364  ssrnres  5368  sofld  5377  funssxp  5665  fssres  5672  dff2  5958  dff3  5959  fliftf  6132  1stcof  6745  2ndcof  6746  frxp  6827  smores  6959  fodomfi  7732  marypha1lem  7826  marypha1  7827  dfac12lem2  8455  brdom4  8839  smobeth  8892  fpwwe2lem13  8949  nqerf  9237  prdsval  14881  prdsbas  14883  prdsplusg  14884  prdsmulr  14885  prdsvsca  14886  prdshom  14893  catcoppccl  15523  catcfuccl  15524  catcxpccl  15612  lern  15991  odf1o2  16729  gsumzres  17050  gsumzresOLD  17054  gsumzaddlem  17070  gsumzadd  17071  gsumzaddlemOLD  17072  gsumzaddOLD  17073  dprdfadd  17192  dprdfaddOLD  17199  dprdres  17207  lmss  19904  txss12  20210  txbasval  20211  txkgen  20257  fmss  20551  tsmsxplem1  20759  ustimasn  20835  utopbas  20842  metustexhalfOLD  21170  metustexhalf  21171  causs  21841  ovoliunlem1  22017  dvcnvrelem1  22522  taylf  22860  dvlog  23138  perpln2  24229  sspba  25778  rntrclfvOAI  27499  imadifxp  27621  metideq  28057  sxbrsigalem5  28451  omsmon  28461  carsggect  28481  carsgclctunlem2  28482  nodenselem6  29647  fixssrn  29746  heicant  30250  mblfinlem1  30252  diophrw  30893  dnnumch2  31193  lmhmlnmsplit  31235  hbtlem6  31282  fourierdlem42  32132  dicval  37351  dfrcl2  38246  relexpss1d  38270  rp-imass  38300