Theorem rnss 4964

Description: Subset theorem for range. (Contributed by NM, 22-Mar-1998.)

Assertion

Ref	Expression
rnss	⊢ (𝐴 ⊆ 𝐵 → ran 𝐴 ⊆ ran 𝐵)

Proof of Theorem rnss

Step	Hyp	Ref	Expression
1		cnvss 4905	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵)
2		dmss 4932	. . 3 ⊢ (◡𝐴 ⊆ ◡𝐵 → dom ◡𝐴 ⊆ dom ◡𝐵)
3	1, 2	syl 14	. 2 ⊢ (𝐴 ⊆ 𝐵 → dom ◡𝐴 ⊆ dom ◡𝐵)
4		df-rn 4738	. 2 ⊢ ran 𝐴 = dom ◡𝐴
5		df-rn 4738	. 2 ⊢ ran 𝐵 = dom ◡𝐵
6	3, 4, 5	3sstr4g 3269	1 ⊢ (𝐴 ⊆ 𝐵 → ran 𝐴 ⊆ ran 𝐵)

Syntax hints:   → wi 4   ⊆ wss 3199  ^◡ccnv 4726  dom cdm 4727  ran crn 4728

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-v 2803  df-un 3203  df-in 3205  df-ss 3212  df-sn 3676  df-pr 3677  df-op 3679  df-br 4090  df-opab 4152  df-cnv 4735  df-dm 4737  df-rn 4738

This theorem is referenced by:  imass1  5113  imass2  5114  rnxpss2  5172  ssxpbm  5174  ssxp2  5176  ssrnres  5181  funssxp  5506  fssres  5514  dff2  5794  fliftf  5945  1stcof  6331  2ndcof  6332  smores  6463  tfrcllembfn  6528  caserel  7291  frecuzrdgtcl  10680  prdsvallem  13378  prdsval  13379  lmss  14999  txss12  15019  txbasval  15020  subgrprop3  16142