MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fssxp Structured version   Visualization version   GIF version

Theorem fssxp 6684
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 (𝐹:𝐴𝐵𝐹 ⊆ (𝐴 × 𝐵))

Proof of Theorem fssxp
StepHypRef Expression
1 frel 6662 . . 3 (𝐹:𝐴𝐵 → Rel 𝐹)
2 relssdmrn 6222 . . 3 (Rel 𝐹𝐹 ⊆ (dom 𝐹 × ran 𝐹))
31, 2syl 17 . 2 (𝐹:𝐴𝐵𝐹 ⊆ (dom 𝐹 × ran 𝐹))
4 fdm 6666 . . . 4 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
5 eqimss 3975 . . . 4 (dom 𝐹 = 𝐴 → dom 𝐹𝐴)
64, 5syl 17 . . 3 (𝐹:𝐴𝐵 → dom 𝐹𝐴)
7 frn 6664 . . 3 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
8 xpss12 5635 . . 3 ((dom 𝐹𝐴 ∧ ran 𝐹𝐵) → (dom 𝐹 × ran 𝐹) ⊆ (𝐴 × 𝐵))
96, 7, 8syl2anc 585 . 2 (𝐹:𝐴𝐵 → (dom 𝐹 × ran 𝐹) ⊆ (𝐴 × 𝐵))
103, 9sstrd 3927 1 (𝐹:𝐴𝐵𝐹 ⊆ (𝐴 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wss 3885   × cxp 5618  dom cdm 5620  ran crn 5621  Rel wrel 5625  wf 6483
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707  ax-sep 5220  ax-pr 5364
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-ral 3050  df-rex 3060  df-rab 3388  df-v 3429  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-br 5075  df-opab 5137  df-xp 5626  df-rel 5627  df-cnv 5628  df-dm 5630  df-rn 5631  df-fun 6489  df-fn 6490  df-f 6491
This theorem is referenced by:  funssxp  6685  opelf  6690  dff2  7040  dff3  7041  fndifnfp  7120  fex2  7876  fabexd  7877  fabexgOLD  7879  f2ndf  8059  f1o2ndf1  8061  mapexOLD  8768  fsetsspwxp  8789  uniixp  8858  wdom2d  9484  rankfu  9790  dfac12lem2  10056  infmap2  10128  axdc3lem  10361  fnct  10448  tskcard  10693  ixxex  13298  imasvscafn  17490  imasvscaf  17492  fnmrc  17562  mrcfval  17563  isacs1i  17612  mreacs  17613  pjfval  21675  pjpm  21677  isngp2  24550  volf  25484  fgraphopab  43619  dfno2  43843  issmflem  47143
  Copyright terms: Public domain W3C validator