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

Theorem fmpt2 6750
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 6749 . 2  |-  ( A. x  e.  A  A. y  e.  B  C  e.  D  <->  F : U_ x  e.  A  ( {
x }  X.  B
) --> D )
3 iunxpconst 5002 . . 3  |-  U_ x  e.  A  ( {
x }  X.  B
)  =  ( A  X.  B )
43feq2i 5659 . 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 1370    e. wcel 1758   A.wral 2798   {csn 3984   U_ciun 4278    X. cxp 4945   -->wf 5521    |-> cmpt2 6201
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638  ax-un 6481
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-sbc 3293  df-csb 3395  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-iun 4280  df-br 4400  df-opab 4458  df-mpt 4459  df-id 4743  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960  df-iota 5488  df-fun 5527  df-fn 5528  df-f 5529  df-fv 5533  df-oprab 6203  df-mpt2 6204  df-1st 6686  df-2nd 6687
This theorem is referenced by:  fnmpt2  6751  fmpt2co  6765  eroprf  7307  omxpenlem  7521  mapxpen  7586  dffi3  7791  ixpiunwdom  7916  cantnfvalf  7983  iunfictbso  8394  axdc4lem  8734  axcclem  8736  addpqf  9223  mulpqf  9225  subf  9722  xaddf  11304  xmulf  11345  ixxf  11420  ioof  11503  fzf  11557  fzof  11666  axdc4uzlem  11920  sadcf  13766  smupf  13791  gcdf  13820  eucalgf  13875  vdwapf  14150  prdsval  14511  prdsplusg  14514  prdsmulr  14515  prdsvsca  14516  prdsds  14520  prdshom  14523  imasvscaf  14595  xpsff1o  14624  wunnat  14984  catcoppccl  15094  catcfuccl  15095  catcxpccl  15135  evlfcl  15150  hofcl  15187  plusffval  15545  mndplusf  15549  grpsubf  15723  subgga  15936  lactghmga  16027  sylow1lem2  16218  sylow3lem1  16246  lsmssv  16262  lsmidm  16281  efgmf  16330  efgtf  16339  frgpuptf  16387  scaffval  17088  lmodscaf  17092  evlslem2  17720  xrsds  17980  ipffval  18201  phlipf  18205  mamucl  18425  mamudiagcl  18426  matbas2d  18448  ordtbas2  18926  iccordt  18949  txuni2  19269  xkotf  19289  txbasval  19310  tx1stc  19354  xkococn  19364  cnmpt12  19371  cnmpt21  19375  cnmpt2t  19377  cnmpt22  19378  cnmptcom  19382  cnmpt2k  19392  txswaphmeo  19509  xpstopnlem1  19513  cnmpt2plusg  19790  cnmpt2vsca  19900  prdsdsf  20073  blfvalps  20089  blfps  20112  blf  20113  stdbdmet  20222  met2ndci  20228  dscmet  20296  xrsxmet  20517  cnmpt2ds  20551  cnmpt2pc  20631  iimulcn  20641  ishtpy  20675  reparphti  20700  cnmpt2ip  20891  bcthlem5  20970  rrxmet  21038  dyadf  21203  itg1addlem2  21307  mbfi1fseqlem1  21325  mbfi1fseqlem3  21327  mbfi1fseqlem4  21328  mbfi1fseqlem5  21329  cxpcn3  22318  sgmf  22615  grpodivf  23884  nvmf  24177  ipf  24262  hvsubf  24568  ofoprabco  26132  sseqfv2  26920  cvxscon  27275  cvmlift2lem5  27339  mblfinlem1  28575  mblfinlem2  28576  sdclem1  28786  metf1o  28798  rrnval  28873  rrnmet  28875  frmx  29401  frmy  29402
  Copyright terms: Public domain W3C validator