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

Theorem fssxp 6595
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 6572 . . 3 (𝐹:𝐴𝐵 → Rel 𝐹)
2 relssdmrn 6150 . . 3 (Rel 𝐹𝐹 ⊆ (dom 𝐹 × ran 𝐹))
31, 2syl 17 . 2 (𝐹:𝐴𝐵𝐹 ⊆ (dom 𝐹 × ran 𝐹))
4 fdm 6576 . . . 4 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
5 eqimss 3974 . . . 4 (dom 𝐹 = 𝐴 → dom 𝐹𝐴)
64, 5syl 17 . . 3 (𝐹:𝐴𝐵 → dom 𝐹𝐴)
7 frn 6574 . . 3 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
8 xpss12 5584 . . 3 ((dom 𝐹𝐴 ∧ ran 𝐹𝐵) → (dom 𝐹 × ran 𝐹) ⊆ (𝐴 × 𝐵))
96, 7, 8syl2anc 587 . 2 (𝐹:𝐴𝐵 → (dom 𝐹 × ran 𝐹) ⊆ (𝐴 × 𝐵))
103, 9sstrd 3928 1 (𝐹:𝐴𝐵𝐹 ⊆ (𝐴 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1543  wss 3883   × cxp 5567  dom cdm 5569  ran crn 5570  Rel wrel 5574  wf 6397
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-12 2177  ax-ext 2710  ax-sep 5209  ax-nul 5216  ax-pr 5339
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2717  df-cleq 2731  df-clel 2818  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3425  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4255  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-xp 5575  df-rel 5576  df-cnv 5577  df-dm 5579  df-rn 5580  df-fun 6403  df-fn 6404  df-f 6405
This theorem is referenced by:  funssxp  6596  opelf  6602  dff2  6940  dff3  6941  fndifnfp  7013  fex2  7733  fabexg  7734  f2ndf  7911  f1o2ndf1  7913  mapex  8538  fsetsspwxp  8558  uniixp  8626  wdom2d  9226  rankfu  9523  dfac12lem2  9788  infmap2  9862  axdc3lem  10094  fnct  10181  tskcard  10425  ixxex  12976  imasvscafn  17075  imasvscaf  17077  fnmrc  17143  mrcfval  17144  isacs1i  17193  mreacs  17194  pjfval  20701  pjpm  20703  isngp2  23527  volf  24458  fgraphopab  40786  issmflem  43981
  Copyright terms: Public domain W3C validator