Theorem fssxp 5591

Description: A mapping is a class of ordered pairs. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)

Assertion

Ref	Expression
fssxp	|- ( F : A --> B -> F C_ ( A X. B ) )

Proof of Theorem fssxp

Step	Hyp	Ref	Expression
1		frel 5583	. . 3 |- ( F : A --> B -> Rel F )
2		relssdmrn 5379	. . 3 |- ( Rel F -> F C_ ( dom F X. ran F ) )
3	1, 2	syl 16	. 2 |- ( F : A --> B -> F C_ ( dom F X. ran F ) )
4		fdm 5584	. . . 4 |- ( F : A --> B -> dom F = A )
5		eqimss 3429	. . . 4 |- ( dom F = A -> dom F C_ A )
6	4, 5	syl 16	. . 3 |- ( F : A --> B -> dom F C_ A )
7		frn 5586	. . 3 |- ( F : A --> B -> ran F C_ B )
8		xpss12 4966	. . 3 |- ( ( dom F C_ A /\ ran F C_ B ) -> ( dom F X. ran F ) C_ ( A X. B ) )
9	6, 7, 8	syl2anc 661	. 2 |- ( F : A --> B -> ( dom F X. ran F ) C_ ( A X. B ) )
10	3, 9	sstrd 3387	1 |- ( F : A --> B -> F C_ ( A X. B ) )

Syntax hints:   -> wi 4   = wceq 1369   C_ wss 3349   X. cxp 4859   dom cdm 4861   ran crn 4862   Rel wrel 4866   -->wf 5435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pr 4552

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-br 4314  df-opab 4372  df-xp 4867  df-rel 4868  df-cnv 4869  df-dm 4871  df-rn 4872  df-fun 5441  df-fn 5442  df-f 5443

This theorem is referenced by:  funssxp  5592  opelf  5595  dff2  5876  dff3  5877  fndifnfp  5928  fex2  6553  fabexg  6554  f2ndf  6699  f1o2ndf1  6701  mapex  7241  uniixp  7307  hartogslem1  7777  wdom2d  7816  rankfu  8105  dfac12lem2  8334  infmap2  8408  axdc3lem  8640  tskcard  8969  dfle2  11145  ixxex  11332  imasvscafn  14496  imasvscaf  14498  fnmrc  14566  mrcfval  14567  isacs1i  14616  mreacs  14617  pjfval  18153  pjpm  18155  hausdiag  19240  isngp2  20211  volf  21034  fnct  26035  fgraphopab  29604