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

Theorem fmpt2 6887
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  |-  F  =  ( x  e.  A ,  y  e.  B  |->  C )
Assertion
Ref Expression
fmpt2  |-  ( A. x  e.  A  A. y  e.  B  C  e.  D  <->  F : ( A  X.  B ) --> D )
Distinct variable groups:    x, A, y    x, B, y    x, D, y
Allowed substitution hints:    C( x, y)    F( x, y)

Proof of Theorem fmpt2
StepHypRef Expression
1 fmpt2.1 . . 3  |-  F  =  ( x  e.  A ,  y  e.  B  |->  C )
21fmpt2x 6886 . 2  |-  ( A. x  e.  A  A. y  e.  B  C  e.  D  <->  F : U_ x  e.  A  ( {
x }  X.  B
) --> D )
3 iunxpconst 4910 . . 3  |-  U_ x  e.  A  ( {
x }  X.  B
)  =  ( A  X.  B )
43feq2i 5743 . 2  |-  ( F : U_ x  e.  A  ( { x }  X.  B ) --> D  <-> 
F : ( A  X.  B ) --> D )
52, 4bitri 257 1  |-  ( A. x  e.  A  A. y  e.  B  C  e.  D  <->  F : ( A  X.  B ) --> D )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    = wceq 1455    e. wcel 1898   A.wral 2749   {csn 3980   U_ciun 4292    X. cxp 4851   -->wf 5597    |-> cmpt2 6317
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-fv 5609  df-oprab 6319  df-mpt2 6320  df-1st 6820  df-2nd 6821
This theorem is referenced by:  fnmpt2  6888  ovmpt2elrn  6891  fmpt2co  6906  eroprf  7487  omxpenlem  7699  mapxpen  7764  dffi3  7971  ixpiunwdom  8132  cantnfvalf  8196  iunfictbso  8571  axdc4lem  8911  axcclem  8913  addpqf  9395  mulpqf  9397  subf  9903  xaddf  11546  xmulf  11587  ixxf  11674  ioof  11761  fzf  11817  fzof  11948  axdc4uzlem  12227  sadcf  14476  smupf  14501  gcdf  14532  eucalgf  14591  vdwapf  14971  prdsval  15402  prdsplusg  15405  prdsmulr  15406  prdsvsca  15407  prdsds  15411  prdshom  15414  imasvscaf  15494  xpsff1o  15523  wunnat  15910  catcoppccl  16052  catcfuccl  16053  catcxpccl  16141  evlfcl  16156  hofcl  16193  plusffval  16542  mgmplusf  16546  grpsubf  16782  subgga  17003  lactghmga  17094  sylow1lem2  17300  sylow3lem1  17328  lsmssv  17344  lsmidm  17363  efgmf  17412  efgtf  17421  frgpuptf  17469  scaffval  18158  lmodscaf  18162  evlslem2  18784  xrsds  19060  ipffval  19264  phlipf  19268  mamucl  19475  matbas2d  19497  mamumat1cl  19513  ordtbas2  20256  iccordt  20279  txuni2  20629  xkotf  20649  txbasval  20670  tx1stc  20714  xkococn  20724  cnmpt12  20731  cnmpt21  20735  cnmpt2t  20737  cnmpt22  20738  cnmptcom  20742  cnmpt2k  20752  txswaphmeo  20869  xpstopnlem1  20873  cnmpt2plusg  21152  cnmpt2vsca  21258  prdsdsf  21431  blfvalps  21447  blfps  21470  blf  21471  stdbdmet  21580  met2ndci  21586  dscmet  21636  xrsxmet  21876  cnmpt2ds  21910  cnmpt2pc  22005  iimulcn  22015  ishtpy  22052  reparphti  22077  cnmpt2ip  22268  bcthlem5  22345  rrxmet  22411  dyadf  22598  itg1addlem2  22704  mbfi1fseqlem1  22722  mbfi1fseqlem3  22724  mbfi1fseqlem4  22725  mbfi1fseqlem5  22726  cxpcn3  23737  sgmf  24121  midf  24867  grpodivf  26023  nvmf  26316  ipf  26401  hvsubf  26717  ofoprabco  28316  sitmf  29234  sseqfv2  29276  cvxscon  30015  cvmlift2lem5  30079  mblfinlem1  32022  mblfinlem2  32023  sdclem1  32117  metf1o  32129  rrnval  32204  rrnmet  32206  frmx  35806  frmy  35807
  Copyright terms: Public domain W3C validator