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

Theorem fmpt2 6630
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 6629 . 2  |-  ( A. x  e.  A  A. y  e.  B  C  e.  D  <->  F : U_ x  e.  A  ( {
x }  X.  B
) --> D )
3 iunxpconst 4882 . . 3  |-  U_ x  e.  A  ( {
x }  X.  B
)  =  ( A  X.  B )
43feq2i 5540 . 2  |-  ( F : U_ x  e.  A  ( { x }  X.  B ) --> D  <-> 
F : ( A  X.  B ) --> D )
52, 4bitri 249 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 184    = wceq 1362    e. wcel 1755   A.wral 2705   {csn 3865   U_ciun 4159    X. cxp 4825   -->wf 5402    e. cmpt2 6082
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-fv 5414  df-oprab 6084  df-mpt2 6085  df-1st 6566  df-2nd 6567
This theorem is referenced by:  fnmpt2  6631  fmpt2co  6645  eroprf  7186  omxpenlem  7400  mapxpen  7465  dffi3  7669  ixpiunwdom  7794  cantnfvalf  7861  iunfictbso  8272  axdc4lem  8612  axcclem  8614  addpqf  9101  mulpqf  9103  subf  9600  xaddf  11182  xmulf  11223  ixxf  11298  ioof  11375  fzf  11428  fzof  11534  axdc4uzlem  11788  sadcf  13632  smupf  13657  gcdf  13686  eucalgf  13741  vdwapf  14016  prdsval  14376  prdsplusg  14379  prdsmulr  14380  prdsvsca  14381  prdsds  14385  prdshom  14388  imasvscaf  14460  xpsff1o  14489  wunnat  14849  catcoppccl  14959  catcfuccl  14960  catcxpccl  15000  evlfcl  15015  hofcl  15052  plusffval  15410  mndplusf  15414  grpsubf  15585  subgga  15798  lactghmga  15889  sylow1lem2  16078  sylow3lem1  16106  lsmssv  16122  lsmidm  16141  efgmf  16190  efgtf  16199  frgpuptf  16247  scaffval  16890  lmodscaf  16894  evlslem2  17525  xrsds  17700  ipffval  17919  phlipf  17923  mamucl  18143  mamudiagcl  18144  matbas2d  18166  ordtbas2  18637  iccordt  18660  txuni2  18980  xkotf  19000  txbasval  19021  tx1stc  19065  xkococn  19075  cnmpt12  19082  cnmpt21  19086  cnmpt2t  19088  cnmpt22  19089  cnmptcom  19093  cnmpt2k  19103  txswaphmeo  19220  xpstopnlem1  19224  cnmpt2plusg  19501  cnmpt2vsca  19611  prdsdsf  19784  blfvalps  19800  blfps  19823  blf  19824  stdbdmet  19933  met2ndci  19939  dscmet  20007  xrsxmet  20228  cnmpt2ds  20262  cnmpt2pc  20342  iimulcn  20352  ishtpy  20386  reparphti  20411  cnmpt2ip  20602  bcthlem5  20681  rrxmet  20749  dyadf  20913  itg1addlem2  21017  mbfi1fseqlem1  21035  mbfi1fseqlem3  21037  mbfi1fseqlem4  21038  mbfi1fseqlem5  21039  cxpcn3  22071  sgmf  22368  grpodivf  23556  nvmf  23849  ipf  23934  hvsubf  24240  ofoprabco  25806  sseqfv2  26625  cvxscon  26980  cvmlift2lem5  27044  mblfinlem1  28272  mblfinlem2  28273  sdclem1  28483  metf1o  28495  rrnval  28570  rrnmet  28572  frmx  29099  frmy  29100
  Copyright terms: Public domain W3C validator