Theorem fnmpt2i 7239

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

Step	Hyp	Ref	Expression
1		fnmpt2i.2	. . 3 |- C e. _V
2	1	rgen2w 2925	. 2 |- A. x e. A A. y e. B C e. _V
3		fmpt2.1	. . 3 |- F = ( x e. A , y e. B |-> C )
4	3	fnmpt2 7238	. 2 |- ( A. x e. A A. y e. B C e. _V -> F Fn ( A X. B ) )
5	2, 4	ax-mp 5	1 |- F Fn ( A X. B )

Syntax hints:   = wceq 1483   e. wcel 1990   A.wral 2912   _Vcvv 3200   X. cxp 5112   Fn wfn 5883   |-> cmpt2 6652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896  df-oprab 6654  df-mpt2 6655  df-1st 7168  df-2nd 7169

This theorem is referenced by:  dmmpt2  7240  fnoa  7588  fnom  7589  fnoe  7590  fnmap  7864  fnpm  7865  cdafn  8991  addpqnq  9760  mulpqnq  9763  elq  11790  cnref1o  11827  ccatfn  13357  qnnen  14942  restfn  16085  prdsdsfn  16125  imasdsfn  16174  imasvscafn  16197  homffn  16353  comfffn  16364  comffn  16365  isoval  16425  cofucl  16548  fnfuc  16605  natffn  16609  catcisolem  16756  estrchomfn  16775  funcestrcsetclem4  16783  funcsetcestrclem4  16798  fnxpc  16816  1stfcl  16837  2ndfcl  16838  prfcl  16843  evlfcl  16862  curf1cl  16868  curfcl  16872  hofcl  16899  yonedalem3  16920  yonedainv  16921  plusffn  17250  mulgfval  17542  mulgfn  17544  gimfn  17703  symgplusg  17809  sylow2blem2  18036  scaffn  18884  lmimfn  19026  mplsubrglem  19439  ipffn  19996  tx1stc  21453  tx2ndc  21454  hmeofn  21560  symgtgp  21905  qustgplem  21924  nmoffn  22515  rrxmfval  23189  mbfimaopnlem  23422  i1fadd  23462  i1fmul  23463  smatrcl  29862  txomap  29901  qtophaus  29903  pstmxmet  29940  dya2icoseg  30339  dya2iocrfn  30341  fncvm  31239  cntotbnd  33595  rnghmfn  41890  rhmfn  41918  rnghmsscmap2  41973  rnghmsscmap  41974  rngchomffvalALTV  41995  rngchomrnghmresALTV  41996  rhmsscmap2  42019  rhmsscmap  42020  funcringcsetcALTV2lem4  42039  funcringcsetclem4ALTV  42062  srhmsubc  42076  fldc  42083  fldhmsubc  42084  rhmsubclem1  42086  srhmsubcALTV  42094  fldcALTV  42101  fldhmsubcALTV  42102  rhmsubcALTVlem1  42104