ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rnss GIF version

Theorem rnss 4635
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 4579 . . 3 (𝐴𝐵𝐴𝐵)
2 dmss 4605 . . 3 (𝐴𝐵 → dom 𝐴 ⊆ dom 𝐵)
31, 2syl 14 . 2 (𝐴𝐵 → dom 𝐴 ⊆ dom 𝐵)
4 df-rn 4424 . 2 ran 𝐴 = dom 𝐴
5 df-rn 4424 . 2 ran 𝐵 = dom 𝐵
63, 4, 53sstr4g 3056 1 (𝐴𝐵 → ran 𝐴 ⊆ ran 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wss 2988  ccnv 4412  dom cdm 4413  ran crn 4414
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-un 2992  df-in 2994  df-ss 3001  df-sn 3437  df-pr 3438  df-op 3440  df-br 3823  df-opab 3877  df-cnv 4421  df-dm 4423  df-rn 4424
This theorem is referenced by:  imass1  4776  imass2  4777  rnxpss2  4832  ssxpbm  4834  ssxp2  4836  ssrnres  4841  funssxp  5146  fssres  5152  dff2  5408  fliftf  5541  1stcof  5893  2ndcof  5894  smores  6013  tfrcllembfn  6078  caserel  6725  frecuzrdgtcl  9750
  Copyright terms: Public domain W3C validator