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

Theorem fnmpt2i 6646
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 2787 . 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 6645 . 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 1369    e. wcel 1756   A.wral 2718   _Vcvv 2975    X. cxp 4841    Fn wfn 5416    e. cmpt2 6096
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4416  ax-nul 4424  ax-pow 4473  ax-pr 4534  ax-un 6375
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-ral 2723  df-rex 2724  df-rab 2727  df-v 2977  df-sbc 3190  df-csb 3292  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-nul 3641  df-if 3795  df-sn 3881  df-pr 3883  df-op 3887  df-uni 4095  df-iun 4176  df-br 4296  df-opab 4354  df-mpt 4355  df-id 4639  df-xp 4849  df-rel 4850  df-cnv 4851  df-co 4852  df-dm 4853  df-rn 4854  df-res 4855  df-ima 4856  df-iota 5384  df-fun 5423  df-fn 5424  df-f 5425  df-fv 5429  df-oprab 6098  df-mpt2 6099  df-1st 6580  df-2nd 6581
This theorem is referenced by:  dmmpt2  6647  fnoa  6951  fnom  6952  fnoe  6953  fnmap  7224  fnpm  7225  cdafn  8341  addpqnq  9110  mulpqnq  9113  elq  10958  cnref1o  10989  ccatfn  12275  qnnen  13499  restfn  14366  prdsdsfn  14406  imasdsfn  14455  imasvscafn  14478  homffn  14635  comfffn  14646  comffn  14647  isoval  14706  cofucl  14801  fnfuc  14858  natffn  14862  catcisolem  14977  fnxpc  14989  1stfcl  15010  2ndfcl  15011  prfcl  15016  evlfcl  15035  curf1cl  15041  curfcl  15045  hofcl  15072  yonedalem3  15093  yonedainv  15094  plusffn  15433  mulgfval  15631  mulgfn  15633  gimfn  15792  symgplusg  15897  sylow2blem2  16123  scaffn  16972  lmimfn  17110  mplsubrglem  17520  mplsubrglemOLD  17521  ipffn  18083  tx1stc  19226  tx2ndc  19227  hmeofn  19333  symgtgp  19675  divstgplem  19694  nmoffn  20293  rrxmfval  20908  mbfimaopnlem  21136  i1fadd  21176  i1fmul  21177  dya2icoseg  26695  dya2iocrfn  26697  fncvm  27149  cntotbnd  28698
  Copyright terms: Public domain W3C validator