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

Theorem fmpt2 6191
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 6190 . 2  |-  ( A. x  e.  A  A. y  e.  B  C  e.  D  <->  F : U_ x  e.  A  ( {
x }  X.  B
) --> D )
3 iunxpconst 4746 . . 3  |-  U_ x  e.  A  ( {
x }  X.  B
)  =  ( A  X.  B )
43feq2i 5384 . 2  |-  ( F : U_ x  e.  A  ( { x }  X.  B ) --> D  <-> 
F : ( A  X.  B ) --> D )
52, 4bitri 240 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 176    = wceq 1623    e. wcel 1684   A.wral 2543   {csn 3640   U_ciun 3905    X. cxp 4687   -->wf 5251    e. cmpt2 5860
This theorem is referenced by:  fnmpt2  6192  fmpt2co  6202  eroprf  6756  omxpenlem  6963  mapxpen  7027  dffi3  7184  ixpiunwdom  7305  cantnfvalf  7366  iunfictbso  7741  axdc4lem  8081  axcclem  8083  addpqf  8568  mulpqf  8570  subf  9053  xaddf  10551  xmulf  10592  ixxf  10666  ioof  10741  fzf  10786  fzof  10872  axdc4uzlem  11044  sadcf  12644  smupf  12669  gcdf  12698  eucalgf  12753  vdwapf  13019  prdsval  13355  prdsplusg  13358  prdsmulr  13359  prdsvsca  13360  prdsds  13363  prdshom  13366  imasvscaf  13441  xpsff1o  13470  wunnat  13830  catcoppccl  13940  catcfuccl  13941  catcxpccl  13981  evlfcl  13996  hofcl  14033  plusffval  14379  mndplusf  14383  grpsubf  14545  subgga  14754  lactghmga  14784  sylow1lem2  14910  sylow3lem1  14938  lsmssv  14954  lsmidm  14973  efgmf  15022  efgtf  15031  frgpuptf  15079  scaffval  15645  lmodscaf  15649  evlslem2  16249  xrsds  16414  ipffval  16552  phlipf  16556  ordtbas2  16921  iccordt  16944  txuni2  17260  xkotf  17280  txbasval  17301  tx1stc  17344  xkococn  17354  cnmpt12  17361  cnmpt21  17365  cnmpt2t  17367  cnmpt22  17368  cnmptcom  17372  cnmpt2k  17382  txswaphmeo  17496  xpstopnlem1  17500  cnmpt2plusg  17771  cnmpt2vsca  17877  prdsdsf  17931  blfval  17947  blf  17961  stdbdmet  18062  met2ndci  18068  dscmet  18095  xrsxmet  18315  cnmpt2ds  18348  cnmpt2pc  18426  iimulcn  18436  ishtpy  18470  reparphti  18495  cnmpt2ip  18675  bcthlem5  18750  dyadf  18946  itg1addlem2  19052  mbfi1fseqlem1  19070  mbfi1fseqlem3  19072  mbfi1fseqlem4  19073  mbfi1fseqlem5  19074  cxpcn3  20088  sgmf  20383  grpodivf  20913  nvmf  21204  ipf  21289  hvsubf  21595  ofoprabco  23232  cvxscon  23774  cvmlift2lem5  23838  hmeogrpi  25536  sigadd  25649  fnmulcv  25684  sdclem1  26453  metf1o  26469  rrnval  26551  rrnmet  26553  frmx  26998  frmy  26999  mamucl  27456  mamudiagcl  27457
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-fv 5263  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123
  Copyright terms: Public domain W3C validator