Theorem rnss 3358

Description: Subset theorem for range.

Assertion

Ref	Expression
rnss	|- (A (_ B -> ran A (_ ran B)

Proof of Theorem rnss

Step	Hyp	Ref	Expression
1		cnvss 3307	. . 3 |- (A (_ B -> `'A (_ `'B)
2		dmss 3326	. . 3 |- (`'A (_ `'B -> dom `' A (_ dom `' B)
3	1, 2	syl 10	. 2 |- (A (_ B -> dom `' A (_ dom `' B)
4		df-rn 3205	. 2 |- ran A = dom `' A
5		df-rn 3205	. 2 |- ran B = dom `' B
6	3, 4, 5	3sstr4g 2113	1 |- (A (_ B -> ran A (_ ran B)

Syntax hints:   -> wi 3   (_ wss 2058  `'ccnv 3185  dom cdm 3186  ran crn 3187

This theorem is referenced by:  imass1 3448  imass2 3449  ssxpr 3491  ssrnres 3497  funssxp 3654  fssres 3659  dff4 3832  dff2 3833  1stcof 4117  mapval2 4353  fodom 4815  brdom4 4820  infxpidmlem7 7591  lmsslem 7978  sspba 8411  rnhmph 10566  relrded 10696  relrcat 10717

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-10 970  ax-11 971  ax-12 972  ax-13 973  ax-14 974  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1127  ax-10o 1144  ax-16 1214  ax-11o 1222  ax-ext 1464  ax-sep 2718  ax-pow 2758  ax-pr 2795

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 985  df-sb 1176  df-eu 1386  df-mo 1387  df-clab 1470  df-cleq 1475  df-clel 1478  df-ne 1594  df-v 1819  df-dif 2060  df-un 2061  df-in 2062  df-ss 2064  df-nul 2292  df-pw 2414  df-sn 2424  df-pr 2425  df-op 2428  df-br 2635  df-opab 2682  df-cnv 3202  df-dm 3204  df-rn 3205

Copyright terms: Public domain