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

Theorem fmpt2 7282
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 7281 . 2 (∀𝑥𝐴𝑦𝐵 𝐶𝐷𝐹: 𝑥𝐴 ({𝑥} × 𝐵)⟶𝐷)
3 iunxpconst 5209 . . 3 𝑥𝐴 ({𝑥} × 𝐵) = (𝐴 × 𝐵)
43feq2i 6075 . 2 (𝐹: 𝑥𝐴 ({𝑥} × 𝐵)⟶𝐷𝐹:(𝐴 × 𝐵)⟶𝐷)
52, 4bitri 264 1 (∀𝑥𝐴𝑦𝐵 𝐶𝐷𝐹:(𝐴 × 𝐵)⟶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1523  wcel 2030  wral 2941  {csn 4210   ciun 4552   × cxp 5141  wf 5922  cmpt2 6692
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-fv 5934  df-oprab 6694  df-mpt2 6695  df-1st 7210  df-2nd 7211
This theorem is referenced by:  fnmpt2  7283  ovmpt2elrn  7286  fmpt2co  7305  eroprf  7888  omxpenlem  8102  mapxpen  8167  dffi3  8378  ixpiunwdom  8537  cantnfvalf  8600  iunfictbso  8975  axdc4lem  9315  axcclem  9317  addpqf  9804  mulpqf  9806  subf  10321  xaddf  12093  xmulf  12140  ixxf  12223  ioof  12309  fzf  12368  fzof  12506  axdc4uzlem  12822  sadcf  15222  smupf  15247  gcdf  15281  eucalgf  15343  vdwapf  15723  prdsval  16162  prdsplusg  16165  prdsmulr  16166  prdsvsca  16167  prdsds  16171  prdshom  16174  imasvscaf  16246  xpsff1o  16275  wunnat  16663  catcoppccl  16805  catcfuccl  16806  catcxpccl  16894  evlfcl  16909  hofcl  16946  plusffval  17294  mgmplusf  17298  grpsubf  17541  subgga  17779  lactghmga  17870  sylow1lem2  18060  sylow3lem1  18088  lsmssv  18104  lsmidm  18123  efgmf  18172  efgtf  18181  frgpuptf  18229  scaffval  18929  lmodscaf  18933  evlslem2  19560  xrsds  19837  ipffval  20041  phlipf  20045  mamucl  20255  matbas2d  20277  mamumat1cl  20293  ordtbas2  21043  iccordt  21066  txuni2  21416  xkotf  21436  txbasval  21457  tx1stc  21501  xkococn  21511  cnmpt12  21518  cnmpt21  21522  cnmpt2t  21524  cnmpt22  21525  cnmptcom  21529  cnmpt2k  21539  txswaphmeo  21656  xpstopnlem1  21660  cnmpt2plusg  21939  cnmpt2vsca  22045  prdsdsf  22219  blfvalps  22235  blfps  22258  blf  22259  stdbdmet  22368  met2ndci  22374  dscmet  22424  xrsxmet  22659  cnmpt2ds  22693  cnmpt2pc  22774  iimulcn  22784  ishtpy  22818  reparphti  22843  cnmpt2ip  23093  bcthlem5  23171  rrxmet  23237  dyadf  23405  itg1addlem2  23509  mbfi1fseqlem1  23527  mbfi1fseqlem3  23529  mbfi1fseqlem4  23530  mbfi1fseqlem5  23531  cxpcn3  24534  sgmf  24916  midf  25713  grpodivf  27520  nvmf  27628  ipf  27696  hvsubf  28000  ofoprabco  29592  sitmf  30542  cvxsconn  31351  cvmlift2lem5  31415  uncf  33518  mblfinlem1  33576  mblfinlem2  33577  sdclem1  33669  metf1o  33681  rrnval  33756  rrnmet  33758  frmx  37795  frmy  37796  icof  39725
  Copyright terms: Public domain W3C validator