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

Theorem fmpt2 6840
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 6839 . 2  |-  ( A. x  e.  A  A. y  e.  B  C  e.  D  <->  F : U_ x  e.  A  ( {
x }  X.  B
) --> D )
3 iunxpconst 5045 . . 3  |-  U_ x  e.  A  ( {
x }  X.  B
)  =  ( A  X.  B )
43feq2i 5706 . 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 1398    e. wcel 1823   A.wral 2804   {csn 4016   U_ciun 4315    X. cxp 4986   -->wf 5566    |-> cmpt2 6272
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-fv 5578  df-oprab 6274  df-mpt2 6275  df-1st 6773  df-2nd 6774
This theorem is referenced by:  fnmpt2  6841  ovmpt2elrn  6844  fmpt2co  6856  eroprf  7401  omxpenlem  7611  mapxpen  7676  dffi3  7883  ixpiunwdom  8009  cantnfvalf  8075  iunfictbso  8486  axdc4lem  8826  axcclem  8828  addpqf  9311  mulpqf  9313  subf  9813  xaddf  11426  xmulf  11467  ixxf  11542  ioof  11625  fzf  11679  fzof  11801  axdc4uzlem  12077  sadcf  14190  smupf  14215  gcdf  14244  eucalgf  14299  vdwapf  14577  prdsval  14947  prdsplusg  14950  prdsmulr  14951  prdsvsca  14952  prdsds  14956  prdshom  14959  imasvscaf  15031  xpsff1o  15060  wunnat  15447  catcoppccl  15589  catcfuccl  15590  catcxpccl  15678  evlfcl  15693  hofcl  15730  plusffval  16079  mgmplusf  16083  grpsubf  16319  subgga  16540  lactghmga  16631  sylow1lem2  16821  sylow3lem1  16849  lsmssv  16865  lsmidm  16884  efgmf  16933  efgtf  16942  frgpuptf  16990  scaffval  17728  lmodscaf  17732  evlslem2  18378  xrsds  18659  ipffval  18859  phlipf  18863  mamucl  19073  matbas2d  19095  mamumat1cl  19111  ordtbas2  19862  iccordt  19885  txuni2  20235  xkotf  20255  txbasval  20276  tx1stc  20320  xkococn  20330  cnmpt12  20337  cnmpt21  20341  cnmpt2t  20343  cnmpt22  20344  cnmptcom  20348  cnmpt2k  20358  txswaphmeo  20475  xpstopnlem1  20479  cnmpt2plusg  20756  cnmpt2vsca  20866  prdsdsf  21039  blfvalps  21055  blfps  21078  blf  21079  stdbdmet  21188  met2ndci  21194  dscmet  21262  xrsxmet  21483  cnmpt2ds  21517  cnmpt2pc  21597  iimulcn  21607  ishtpy  21641  reparphti  21666  cnmpt2ip  21857  bcthlem5  21936  rrxmet  22004  dyadf  22169  itg1addlem2  22273  mbfi1fseqlem1  22291  mbfi1fseqlem3  22293  mbfi1fseqlem4  22294  mbfi1fseqlem5  22295  cxpcn3  23293  sgmf  23620  midf  24346  grpodivf  25449  nvmf  25742  ipf  25827  hvsubf  26133  ofoprabco  27735  sseqfv2  28600  cvxscon  28955  cvmlift2lem5  29019  mblfinlem1  30294  mblfinlem2  30295  sdclem1  30479  metf1o  30491  rrnval  30566  rrnmet  30568  frmx  31091  frmy  31092
  Copyright terms: Public domain W3C validator