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

Theorem fssxp 6756
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 6732 . . 3 (𝐹:𝐴𝐵 → Rel 𝐹)
2 relssdmrn 6277 . . 3 (Rel 𝐹𝐹 ⊆ (dom 𝐹 × ran 𝐹))
31, 2syl 17 . 2 (𝐹:𝐴𝐵𝐹 ⊆ (dom 𝐹 × ran 𝐹))
4 fdm 6736 . . . 4 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
5 eqimss 4040 . . . 4 (dom 𝐹 = 𝐴 → dom 𝐹𝐴)
64, 5syl 17 . . 3 (𝐹:𝐴𝐵 → dom 𝐹𝐴)
7 frn 6734 . . 3 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
8 xpss12 5697 . . 3 ((dom 𝐹𝐴 ∧ ran 𝐹𝐵) → (dom 𝐹 × ran 𝐹) ⊆ (𝐴 × 𝐵))
96, 7, 8syl2anc 582 . 2 (𝐹:𝐴𝐵 → (dom 𝐹 × ran 𝐹) ⊆ (𝐴 × 𝐵))
103, 9sstrd 3992 1 (𝐹:𝐴𝐵𝐹 ⊆ (𝐴 × 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1533  wss 3949   × cxp 5680  dom cdm 5682  ran crn 5683  Rel wrel 5687  wf 6549
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pr 5433
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-ral 3059  df-rex 3068  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-br 5153  df-opab 5215  df-xp 5688  df-rel 5689  df-cnv 5690  df-dm 5692  df-rn 5693  df-fun 6555  df-fn 6556  df-f 6557
This theorem is referenced by:  funssxp  6757  opelf  6763  dff2  7114  dff3  7115  fndifnfp  7191  fex2  7947  fabexg  7948  f2ndf  8131  f1o2ndf1  8133  mapex  8857  fsetsspwxp  8878  uniixp  8946  wdom2d  9611  rankfu  9908  dfac12lem2  10175  infmap2  10249  axdc3lem  10481  fnct  10568  tskcard  10812  ixxex  13375  imasvscafn  17526  imasvscaf  17528  fnmrc  17594  mrcfval  17595  isacs1i  17644  mreacs  17645  pjfval  21647  pjpm  21649  isngp2  24526  volf  25478  fgraphopab  42662  dfno2  42889  issmflem  46144
  Copyright terms: Public domain W3C validator