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

Theorem fmpt2 7104
Description: Functionality, domain and range of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.)
Hypothesis
Ref Expression
fmpt2.1 𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)
Assertion
Ref Expression
fmpt2 (∀𝑥𝐴𝑦𝐵 𝐶𝐷𝐹:(𝐴 × 𝐵)⟶𝐷)
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝑥,𝐷,𝑦
Allowed substitution hints:   𝐶(𝑥,𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem fmpt2
StepHypRef Expression
1 fmpt2.1 . . 3 𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)
21fmpt2x 7103 . 2 (∀𝑥𝐴𝑦𝐵 𝐶𝐷𝐹: 𝑥𝐴 ({𝑥} × 𝐵)⟶𝐷)
3 iunxpconst 5088 . . 3 𝑥𝐴 ({𝑥} × 𝐵) = (𝐴 × 𝐵)
43feq2i 5936 . 2 (𝐹: 𝑥𝐴 ({𝑥} × 𝐵)⟶𝐷𝐹:(𝐴 × 𝐵)⟶𝐷)
52, 4bitri 263 1 (∀𝑥𝐴𝑦𝐵 𝐶𝐷𝐹:(𝐴 × 𝐵)⟶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wb 195   = wceq 1475  wcel 1977  wral 2896  {csn 4125   ciun 4450   × cxp 5026  wf 5786  cmpt2 6529
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4704  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4368  df-iun 4452  df-br 4579  df-opab 4639  df-mpt 4640  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-fv 5798  df-oprab 6531  df-mpt2 6532  df-1st 7037  df-2nd 7038
This theorem is referenced by:  fnmpt2  7105  ovmpt2elrn  7108  fmpt2co  7125  eroprf  7710  omxpenlem  7924  mapxpen  7989  dffi3  8198  ixpiunwdom  8357  cantnfvalf  8423  iunfictbso  8798  axdc4lem  9138  axcclem  9140  addpqf  9623  mulpqf  9625  subf  10135  xaddf  11891  xmulf  11934  ixxf  12015  ioof  12101  fzf  12159  fzof  12294  axdc4uzlem  12602  sadcf  14962  smupf  14987  gcdf  15021  eucalgf  15083  vdwapf  15463  prdsval  15887  prdsplusg  15890  prdsmulr  15891  prdsvsca  15892  prdsds  15896  prdshom  15899  imasvscaf  15971  xpsff1o  16000  wunnat  16388  catcoppccl  16530  catcfuccl  16531  catcxpccl  16619  evlfcl  16634  hofcl  16671  plusffval  17019  mgmplusf  17023  grpsubf  17266  subgga  17505  lactghmga  17596  sylow1lem2  17786  sylow3lem1  17814  lsmssv  17830  lsmidm  17849  efgmf  17898  efgtf  17907  frgpuptf  17955  scaffval  18653  lmodscaf  18657  evlslem2  19282  xrsds  19557  ipffval  19760  phlipf  19764  mamucl  19974  matbas2d  19996  mamumat1cl  20012  ordtbas2  20753  iccordt  20776  txuni2  21126  xkotf  21146  txbasval  21167  tx1stc  21211  xkococn  21221  cnmpt12  21228  cnmpt21  21232  cnmpt2t  21234  cnmpt22  21235  cnmptcom  21239  cnmpt2k  21249  txswaphmeo  21366  xpstopnlem1  21370  cnmpt2plusg  21650  cnmpt2vsca  21756  prdsdsf  21930  blfvalps  21946  blfps  21969  blf  21970  stdbdmet  22079  met2ndci  22085  dscmet  22135  xrsxmet  22368  cnmpt2ds  22402  cnmpt2pc  22483  iimulcn  22493  ishtpy  22527  reparphti  22553  cnmpt2ip  22800  bcthlem5  22878  rrxmet  22944  dyadf  23110  itg1addlem2  23215  mbfi1fseqlem1  23233  mbfi1fseqlem3  23235  mbfi1fseqlem4  23236  mbfi1fseqlem5  23237  cxpcn3  24234  sgmf  24616  midf  25414  grpodivf  26570  nvmf  26678  ipf  26746  hvsubf  27050  ofoprabco  28641  sitmf  29535  sseqfv2  29577  cvxscon  30273  cvmlift2lem5  30337  uncf  32352  mblfinlem1  32410  mblfinlem2  32411  sdclem1  32503  metf1o  32515  rrnval  32590  rrnmet  32592  frmx  36290  frmy  36291  icof  38200
  Copyright terms: Public domain W3C validator