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

Theorem rnss 5262
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 5204 . . 3 (𝐴𝐵𝐴𝐵)
2 dmss 5232 . . 3 (𝐴𝐵 → dom 𝐴 ⊆ dom 𝐵)
31, 2syl 17 . 2 (𝐴𝐵 → dom 𝐴 ⊆ dom 𝐵)
4 df-rn 5039 . 2 ran 𝐴 = dom 𝐴
5 df-rn 5039 . 2 ran 𝐵 = dom 𝐵
63, 4, 53sstr4g 3609 1 (𝐴𝐵 → ran 𝐴 ⊆ ran 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3540  ccnv 5027  dom cdm 5028  ran crn 5029
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 4579  df-opab 4639  df-cnv 5036  df-dm 5038  df-rn 5039
This theorem is referenced by:  imass1  5406  imass2  5407  ssxpb  5473  ssrnres  5477  sofld  5486  funssxp  5960  fssres  5968  dff2  6264  dff3  6265  fliftf  6443  1stcof  7065  2ndcof  7066  frxp  7152  smores  7314  fodomfi  8102  marypha1lem  8200  marypha1  8201  dfac12lem2  8827  brdom4  9211  smobeth  9265  fpwwe2lem13  9321  nqerf  9609  prdsval  15887  prdsbas  15889  prdsplusg  15890  prdsmulr  15891  prdsvsca  15892  prdshom  15899  catcoppccl  16530  catcfuccl  16531  catcxpccl  16619  lern  16997  odf1o2  17760  gsumzres  18082  gsumzaddlem  18093  gsumzadd  18094  dprdfadd  18191  dprdres  18199  lmss  20860  txss12  21166  txbasval  21167  txkgen  21213  fmss  21508  tsmsxplem1  21714  ustimasn  21790  utopbas  21797  metustexhalf  22119  causs  22849  ovoliunlem1  23022  dvcnvrelem1  23529  taylf  23864  dvlog  24142  perpln2  25352  sspba  26760  imadifxp  28590  metideq  29058  sxbrsigalem5  29471  omsmon  29481  carsggect  29501  carsgclctunlem2  29502  nodenselem6  30879  fixssrn  30978  heicant  32408  mblfinlem1  32410  dicval  35277  rntrclfvOAI  36066  diophrw  36134  dnnumch2  36427  lmhmlnmsplit  36469  hbtlem6  36512  mptrcllem  36733  cnvrcl0  36745  rntrcl  36748  dfrcl2  36779  relexpss1d  36810  rp-imass  36879  rfovcnvf1od  37112  rnresss  38154  fourierdlem42  38836  sge0less  39079  subgrprop3  40492
  Copyright terms: Public domain W3C validator