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

Theorem fnmpt2i 6868
Description: Functionality and domain of a class given by the "maps to" notation. (Contributed by FL, 17-May-2010.)
Hypotheses
Ref Expression
fmpt2.1  |-  F  =  ( x  e.  A ,  y  e.  B  |->  C )
fnmpt2i.2  |-  C  e. 
_V
Assertion
Ref Expression
fnmpt2i  |-  F  Fn  ( A  X.  B
)
Distinct variable groups:    x, A, y    x, B, y
Allowed substitution hints:    C( x, y)    F( x, y)

Proof of Theorem fnmpt2i
StepHypRef Expression
1 fnmpt2i.2 . . 3  |-  C  e. 
_V
21rgen2w 2819 . 2  |-  A. x  e.  A  A. y  e.  B  C  e.  _V
3 fmpt2.1 . . 3  |-  F  =  ( x  e.  A ,  y  e.  B  |->  C )
43fnmpt2 6867 . 2  |-  ( A. x  e.  A  A. y  e.  B  C  e.  _V  ->  F  Fn  ( A  X.  B
) )
52, 4ax-mp 5 1  |-  F  Fn  ( A  X.  B
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1395    e. wcel 1819   A.wral 2807   _Vcvv 3109    X. cxp 5006    Fn wfn 5589    |-> cmpt2 6298
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-iun 4334  df-br 4457  df-opab 4516  df-mpt 4517  df-id 4804  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-fv 5602  df-oprab 6300  df-mpt2 6301  df-1st 6799  df-2nd 6800
This theorem is referenced by:  dmmpt2  6869  fnoa  7176  fnom  7177  fnoe  7178  fnmap  7445  fnpm  7446  cdafn  8566  addpqnq  9333  mulpqnq  9336  elq  11209  cnref1o  11240  ccatfn  12599  ccatfnOLD  12600  qnnen  13959  restfn  14842  prdsdsfn  14882  imasdsfn  14931  imasvscafn  14954  homffn  15109  comfffn  15120  comffn  15121  isoval  15181  cofucl  15304  fnfuc  15361  natffn  15365  catcisolem  15512  estrchomfn  15531  funcestrcsetclem4  15539  funcsetcestrclem4  15554  fnxpc  15572  1stfcl  15593  2ndfcl  15594  prfcl  15599  evlfcl  15618  curf1cl  15624  curfcl  15628  hofcl  15655  yonedalem3  15676  yonedainv  15677  plusffn  16007  mulgfval  16270  mulgfn  16272  gimfn  16436  symgplusg  16541  sylow2blem2  16768  scaffn  17660  lmimfn  17799  mplsubrglem  18227  mplsubrglemOLD  18228  ipffn  18813  tx1stc  20277  tx2ndc  20278  hmeofn  20384  symgtgp  20726  qustgplem  20745  nmoffn  21344  rrxmfval  21959  mbfimaopnlem  22188  i1fadd  22228  i1fmul  22229  txomap  27998  qtophaus  28000  pstmxmet  28037  dya2icoseg  28421  dya2iocrfn  28423  fncvm  28899  cntotbnd  30476  rnghmfn  32819  rhmfn  32847  rnghmsscmap2  32904  rnghmsscmap  32905  rngchomffvalOLD  32926  rngchomrnghmresOLD  32927  rhmsscmap2  32950  rhmsscmap  32951  funcringcsetcOLD2lem4  32970  funcringcsetclem4OLD  32993  srhmsubc  33007  fldc  33014  fldhmsubc  33015  rhmsubclem1  33017  srhmsubcOLD  33026  fldcOLD  33033  fldhmsubcOLD  33034  rhmsubcOLDlem1  33036
  Copyright terms: Public domain W3C validator