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

Theorem fnmpt2i 6638
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 2778 . 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 6637 . 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 2709   _Vcvv 2966    X. cxp 4830    Fn wfn 5406    e. cmpt2 6088
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 2418  ax-sep 4406  ax-nul 4414  ax-pow 4463  ax-pr 4524  ax-un 6367
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 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2714  df-rex 2715  df-rab 2718  df-v 2968  df-sbc 3180  df-csb 3282  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3631  df-if 3785  df-sn 3871  df-pr 3873  df-op 3877  df-uni 4085  df-iun 4166  df-br 4286  df-opab 4344  df-mpt 4345  df-id 4628  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5374  df-fun 5413  df-fn 5414  df-f 5415  df-fv 5419  df-oprab 6090  df-mpt2 6091  df-1st 6572  df-2nd 6573
This theorem is referenced by:  dmmpt2  6639  fnoa  6940  fnom  6941  fnoe  6942  fnmap  7213  fnpm  7214  cdafn  8330  addpqnq  9099  mulpqnq  9102  elq  10947  cnref1o  10978  ccatfn  12264  qnnen  13488  restfn  14355  prdsdsfn  14395  imasdsfn  14444  imasvscafn  14467  homffn  14624  comfffn  14635  comffn  14636  isoval  14695  cofucl  14790  fnfuc  14847  natffn  14851  catcisolem  14966  fnxpc  14978  1stfcl  14999  2ndfcl  15000  prfcl  15005  evlfcl  15024  curf1cl  15030  curfcl  15034  hofcl  15061  yonedalem3  15082  yonedainv  15083  plusffn  15422  mulgfval  15617  mulgfn  15619  gimfn  15778  symgplusg  15883  sylow2blem2  16109  scaffn  16945  lmimfn  17081  mplsubrglem  17491  mplsubrglemOLD  17492  ipffn  18049  tx1stc  19192  tx2ndc  19193  hmeofn  19299  symgtgp  19641  divstgplem  19660  nmoffn  20259  rrxmfval  20874  mbfimaopnlem  21102  i1fadd  21142  i1fmul  21143  dya2icoseg  26640  dya2iocrfn  26642  fncvm  27094  cntotbnd  28638
  Copyright terms: Public domain W3C validator