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

Theorem fmpt2 6410
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 6409 . 2  |-  ( A. x  e.  A  A. y  e.  B  C  e.  D  <->  F : U_ x  e.  A  ( {
x }  X.  B
) --> D )
3 iunxpconst 4926 . . 3  |-  U_ x  e.  A  ( {
x }  X.  B
)  =  ( A  X.  B )
43feq2i 5578 . 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 1652    e. wcel 1725   A.wral 2697   {csn 3806   U_ciun 4085    X. cxp 4868   -->wf 5442    e. cmpt2 6075
This theorem is referenced by:  fnmpt2  6411  fmpt2co  6422  eroprf  6994  omxpenlem  7201  mapxpen  7265  dffi3  7428  ixpiunwdom  7551  cantnfvalf  7612  iunfictbso  7987  axdc4lem  8327  axcclem  8329  addpqf  8813  mulpqf  8815  subf  9299  xaddf  10802  xmulf  10843  ixxf  10918  ioof  10994  fzf  11039  fzof  11129  axdc4uzlem  11313  sadcf  12957  smupf  12982  gcdf  13011  eucalgf  13066  vdwapf  13332  prdsval  13670  prdsplusg  13673  prdsmulr  13674  prdsvsca  13675  prdsds  13678  prdshom  13681  imasvscaf  13756  xpsff1o  13785  wunnat  14145  catcoppccl  14255  catcfuccl  14256  catcxpccl  14296  evlfcl  14311  hofcl  14348  plusffval  14694  mndplusf  14698  grpsubf  14860  subgga  15069  lactghmga  15099  sylow1lem2  15225  sylow3lem1  15253  lsmssv  15269  lsmidm  15288  efgmf  15337  efgtf  15346  frgpuptf  15394  scaffval  15960  lmodscaf  15964  evlslem2  16560  xrsds  16733  ipffval  16871  phlipf  16875  ordtbas2  17247  iccordt  17270  txuni2  17589  xkotf  17609  txbasval  17630  tx1stc  17674  xkococn  17684  cnmpt12  17691  cnmpt21  17695  cnmpt2t  17697  cnmpt22  17698  cnmptcom  17702  cnmpt2k  17712  txswaphmeo  17829  xpstopnlem1  17833  cnmpt2plusg  18110  cnmpt2vsca  18216  prdsdsf  18389  blfvalps  18405  blfps  18428  blf  18429  stdbdmet  18538  met2ndci  18544  dscmet  18612  xrsxmet  18832  cnmpt2ds  18866  cnmpt2pc  18945  iimulcn  18955  ishtpy  18989  reparphti  19014  cnmpt2ip  19194  bcthlem5  19273  dyadf  19475  itg1addlem2  19581  mbfi1fseqlem1  19599  mbfi1fseqlem3  19601  mbfi1fseqlem4  19602  mbfi1fseqlem5  19603  cxpcn3  20624  sgmf  20920  grpodivf  21826  nvmf  22119  ipf  22204  hvsubf  22510  ofoprabco  24071  cvxscon  24922  cvmlift2lem5  24986  mblfinlem  26234  sdclem1  26438  metf1o  26452  rrnval  26527  rrnmet  26529  frmx  26967  frmy  26968  mamucl  27424  mamudiagcl  27425
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-id 4490  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-fv 5454  df-oprab 6077  df-mpt2 6078  df-1st 6341  df-2nd 6342
  Copyright terms: Public domain W3C validator