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

Theorem fssxp 5955
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 5945 . . 3 (𝐹:𝐴𝐵 → Rel 𝐹)
2 relssdmrn 5555 . . 3 (Rel 𝐹𝐹 ⊆ (dom 𝐹 × ran 𝐹))
31, 2syl 17 . 2 (𝐹:𝐴𝐵𝐹 ⊆ (dom 𝐹 × ran 𝐹))
4 fdm 5946 . . . 4 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
5 eqimss 3615 . . . 4 (dom 𝐹 = 𝐴 → dom 𝐹𝐴)
64, 5syl 17 . . 3 (𝐹:𝐴𝐵 → dom 𝐹𝐴)
7 frn 5948 . . 3 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
8 xpss12 5133 . . 3 ((dom 𝐹𝐴 ∧ ran 𝐹𝐵) → (dom 𝐹 × ran 𝐹) ⊆ (𝐴 × 𝐵))
96, 7, 8syl2anc 690 . 2 (𝐹:𝐴𝐵 → (dom 𝐹 × ran 𝐹) ⊆ (𝐴 × 𝐵))
103, 9sstrd 3573 1 (𝐹:𝐴𝐵𝐹 ⊆ (𝐴 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wss 3535   × cxp 5022  dom cdm 5024  ran crn 5025  Rel wrel 5029  wf 5782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-nul 4708  ax-pr 4824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ral 2896  df-rex 2897  df-rab 2900  df-v 3170  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-sn 4121  df-pr 4123  df-op 4127  df-br 4574  df-opab 4634  df-xp 5030  df-rel 5031  df-cnv 5032  df-dm 5034  df-rn 5035  df-fun 5788  df-fn 5789  df-f 5790
This theorem is referenced by:  funssxp  5956  opelf  5960  dff2  6260  dff3  6261  fndifnfp  6321  fex2  6987  fabexg  6988  f2ndf  7143  f1o2ndf1  7145  mapex  7723  uniixp  7790  hartogslem1  8303  wdom2d  8341  rankfu  8596  dfac12lem2  8822  infmap2  8896  axdc3lem  9128  tskcard  9455  dfle2  11811  ixxex  12009  imasvscafn  15962  imasvscaf  15964  fnmrc  16032  mrcfval  16033  isacs1i  16083  mreacs  16084  pjfval  19807  pjpm  19809  hausdiag  21196  isngp2  22148  volf  23017  fnct  28678  fgraphopab  36606  issmflem  39413
  Copyright terms: Public domain W3C validator