Theorem fssxp 5739

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 5730	. . 3 |- ( F : A --> B -> Rel F )
2		relssdmrn 5355	. . 3 |- ( Rel F -> F C_ ( dom F X. ran F ) )
3	1, 2	syl 17	. 2 |- ( F : A --> B -> F C_ ( dom F X. ran F ) )
4		fdm 5731	. . . 4 |- ( F : A --> B -> dom F = A )
5		eqimss 3483	. . . 4 |- ( dom F = A -> dom F C_ A )
6	4, 5	syl 17	. . 3 |- ( F : A --> B -> dom F C_ A )
7		frn 5733	. . 3 |- ( F : A --> B -> ran F C_ B )
8		xpss12 4939	. . 3 |- ( ( dom F C_ A /\ ran F C_ B ) -> ( dom F X. ran F ) C_ ( A X. B ) )
9	6, 7, 8	syl2anc 666	. 2 |- ( F : A --> B -> ( dom F X. ran F ) C_ ( A X. B ) )
10	3, 9	sstrd 3441	1 |- ( F : A --> B -> F C_ ( A X. B ) )

Syntax hints:   -> wi 4   = wceq 1443   C_ wss 3403   X. cxp 4831   dom cdm 4833   ran crn 4834   Rel wrel 4838   -->wf 5577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pr 4638

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-br 4402  df-opab 4461  df-xp 4839  df-rel 4840  df-cnv 4841  df-dm 4843  df-rn 4844  df-fun 5583  df-fn 5584  df-f 5585

This theorem is referenced by:  funssxp  5740  opelf  5743  dff2  6032  dff3  6033  fndifnfp  6091  fex2  6745  fabexg  6746  f2ndf  6899  f1o2ndf1  6901  mapex  7475  uniixp  7542  hartogslem1  8054  wdom2d  8092  rankfu  8345  dfac12lem2  8571  infmap2  8645  axdc3lem  8877  tskcard  9203  dfle2  11443  ixxex  11643  imasvscafn  15436  imasvscaf  15438  fnmrc  15506  mrcfval  15507  isacs1i  15556  mreacs  15557  pjfval  19262  pjpm  19264  hausdiag  20653  isngp2  21604  volf  22476  fnct  28290  fgraphopab  36081