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

Theorem fmpt2 6350
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 6349 . 2  |-  ( A. x  e.  A  A. y  e.  B  C  e.  D  <->  F : U_ x  e.  A  ( {
x }  X.  B
) --> D )
3 iunxpconst 4867 . . 3  |-  U_ x  e.  A  ( {
x }  X.  B
)  =  ( A  X.  B )
43feq2i 5519 . 2  |-  ( F : U_ x  e.  A  ( { x }  X.  B ) --> D  <-> 
F : ( A  X.  B ) --> D )
52, 4bitri 241 1  |-  ( A. x  e.  A  A. y  e.  B  C  e.  D  <->  F : ( A  X.  B ) --> D )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    = wceq 1649    e. wcel 1717   A.wral 2642   {csn 3750   U_ciun 4028    X. cxp 4809   -->wf 5383    e. cmpt2 6015
This theorem is referenced by:  fnmpt2  6351  fmpt2co  6362  eroprf  6931  omxpenlem  7138  mapxpen  7202  dffi3  7364  ixpiunwdom  7485  cantnfvalf  7546  iunfictbso  7921  axdc4lem  8261  axcclem  8263  addpqf  8747  mulpqf  8749  subf  9232  xaddf  10735  xmulf  10776  ixxf  10851  ioof  10927  fzf  10972  fzof  11060  axdc4uzlem  11241  sadcf  12885  smupf  12910  gcdf  12939  eucalgf  12994  vdwapf  13260  prdsval  13598  prdsplusg  13601  prdsmulr  13602  prdsvsca  13603  prdsds  13606  prdshom  13609  imasvscaf  13684  xpsff1o  13713  wunnat  14073  catcoppccl  14183  catcfuccl  14184  catcxpccl  14224  evlfcl  14239  hofcl  14276  plusffval  14622  mndplusf  14626  grpsubf  14788  subgga  14997  lactghmga  15027  sylow1lem2  15153  sylow3lem1  15181  lsmssv  15197  lsmidm  15216  efgmf  15265  efgtf  15274  frgpuptf  15322  scaffval  15888  lmodscaf  15892  evlslem2  16488  xrsds  16657  ipffval  16795  phlipf  16799  ordtbas2  17170  iccordt  17193  txuni2  17511  xkotf  17531  txbasval  17552  tx1stc  17596  xkococn  17606  cnmpt12  17613  cnmpt21  17617  cnmpt2t  17619  cnmpt22  17620  cnmptcom  17624  cnmpt2k  17634  txswaphmeo  17751  xpstopnlem1  17755  cnmpt2plusg  18032  cnmpt2vsca  18138  prdsdsf  18298  blfval  18314  blf  18328  stdbdmet  18429  met2ndci  18435  dscmet  18484  xrsxmet  18704  cnmpt2ds  18738  cnmpt2pc  18817  iimulcn  18827  ishtpy  18861  reparphti  18886  cnmpt2ip  19066  bcthlem5  19143  dyadf  19343  itg1addlem2  19449  mbfi1fseqlem1  19467  mbfi1fseqlem3  19469  mbfi1fseqlem4  19470  mbfi1fseqlem5  19471  cxpcn3  20492  sgmf  20788  grpodivf  21675  nvmf  21968  ipf  22053  hvsubf  22359  ofoprabco  23914  cvxscon  24702  cvmlift2lem5  24766  sdclem1  26131  metf1o  26145  rrnval  26220  rrnmet  26222  frmx  26660  frmy  26661  mamucl  27118  mamudiagcl  27119
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361  ax-sep 4264  ax-nul 4272  ax-pow 4311  ax-pr 4337  ax-un 4634
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2235  df-mo 2236  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ne 2545  df-ral 2647  df-rex 2648  df-rab 2651  df-v 2894  df-sbc 3098  df-csb 3188  df-dif 3259  df-un 3261  df-in 3263  df-ss 3270  df-nul 3565  df-if 3676  df-sn 3756  df-pr 3757  df-op 3759  df-uni 3951  df-iun 4030  df-br 4147  df-opab 4201  df-mpt 4202  df-id 4432  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5351  df-fun 5389  df-fn 5390  df-f 5391  df-fv 5395  df-oprab 6017  df-mpt2 6018  df-1st 6281  df-2nd 6282
  Copyright terms: Public domain W3C validator