MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rnss Structured version   Visualization version   GIF version

Theorem rnss 5275
Description: Subset theorem for range. (Contributed by NM, 22-Mar-1998.)
Assertion
Ref Expression
rnss (𝐴𝐵 → ran 𝐴 ⊆ ran 𝐵)

Proof of Theorem rnss
StepHypRef Expression
1 cnvss 5216 . . 3 (𝐴𝐵𝐴𝐵)
2 dmss 5245 . . 3 (𝐴𝐵 → dom 𝐴 ⊆ dom 𝐵)
31, 2syl 17 . 2 (𝐴𝐵 → dom 𝐴 ⊆ dom 𝐵)
4 df-rn 5049 . 2 ran 𝐴 = dom 𝐴
5 df-rn 5049 . 2 ran 𝐵 = dom 𝐵
63, 4, 53sstr4g 3609 1 (𝐴𝐵 → ran 𝐴 ⊆ ran 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3540  ccnv 5037  dom cdm 5038  ran crn 5039
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-cnv 5046  df-dm 5048  df-rn 5049
This theorem is referenced by:  imass1  5419  imass2  5420  ssxpb  5487  ssrnres  5491  sofld  5500  funssxp  5974  fssres  5983  dff2  6279  dff3  6280  fliftf  6465  1stcof  7087  2ndcof  7088  frxp  7174  smores  7336  fodomfi  8124  marypha1lem  8222  marypha1  8223  dfac12lem2  8849  brdom4  9233  smobeth  9287  fpwwe2lem13  9343  nqerf  9631  prdsval  15938  prdsbas  15940  prdsplusg  15941  prdsmulr  15942  prdsvsca  15943  prdshom  15950  catcoppccl  16581  catcfuccl  16582  catcxpccl  16670  lern  17048  odf1o2  17811  gsumzres  18133  gsumzaddlem  18144  gsumzadd  18145  dprdfadd  18242  dprdres  18250  lmss  20912  txss12  21218  txbasval  21219  txkgen  21265  fmss  21560  tsmsxplem1  21766  ustimasn  21842  utopbas  21849  metustexhalf  22171  causs  22904  ovoliunlem1  23077  dvcnvrelem1  23584  taylf  23919  dvlog  24197  perpln2  25406  sspba  26966  imadifxp  28796  metideq  29264  sxbrsigalem5  29677  omsmon  29687  carsggect  29707  carsgclctunlem2  29708  nodenselem6  31085  fixssrn  31184  heicant  32614  mblfinlem1  32616  dicval  35483  rntrclfvOAI  36272  diophrw  36340  dnnumch2  36633  lmhmlnmsplit  36675  hbtlem6  36718  mptrcllem  36939  cnvrcl0  36951  rntrcl  36954  dfrcl2  36985  relexpss1d  37016  rp-imass  37085  rfovcnvf1od  37318  rnresss  38360  fourierdlem42  39042  sge0less  39285  subgrprop3  40500
  Copyright terms: Public domain W3C validator