Theorem fnmpoi 7896

Description: Functionality and domain of a class given by the maps-to notation. (Contributed by FL, 17-May-2010.)

Hypotheses

Ref	Expression
fmpo.1	⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
fnmpoi.2	⊢ 𝐶 ∈ V

Assertion

Ref	Expression
fnmpoi	⊢ 𝐹 Fn (𝐴 × 𝐵)

Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦

Allowed substitution hints:   𝐶(𝑥,𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem fnmpoi

Step	Hyp	Ref	Expression
1		fnmpoi.2	. . 3 ⊢ 𝐶 ∈ V
2	1	rgen2w 3078	. 2 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ V
3		fmpo.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
4	3	fnmpo 7895	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ V → 𝐹 Fn (𝐴 × 𝐵))
5	2, 4	ax-mp 5	1 ⊢ 𝐹 Fn (𝐴 × 𝐵)

Syntax hints:   = wceq 1541   ∈ wcel 2109  ∀wral 3065  Vcvv 3430   × cxp 5586   Fn wfn 6425   ∈ cmpo 7270

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355  ax-un 7579

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-iun 4931  df-br 5079  df-opab 5141  df-mpt 5162  df-id 5488  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-fv 6438  df-oprab 7272  df-mpo 7273  df-1st 7817  df-2nd 7818

This theorem is referenced by:  dmmpo  7897  fnoa  8314  fnom  8315  fnoe  8316  fnmap  8596  fnpm  8597  addpqnq  10678  mulpqnq  10681  elq  12672  cnref1o  12707  ccatfn  14256  qnnen  15903  restfn  17116  prdsdsfn  17157  imasdsfn  17206  imasvscafn  17229  homffn  17383  comfffn  17394  comffn  17395  isoval  17458  cofucl  17584  fnfuc  17642  natffn  17646  catcisolem  17806  estrchomfn  17832  funcestrcsetclem4  17841  funcsetcestrclem4  17856  fnxpc  17874  1stfcl  17895  2ndfcl  17896  prfcl  17901  evlfcl  17921  curf1cl  17927  curfcl  17931  hofcl  17958  yonedalem3  17979  yonedainv  17980  plusffn  18316  mulgfval  18683  mulgfvalALT  18684  mulgfn  18686  gimfn  18858  sylow2blem2  19207  scaffn  20125  lmimfn  20269  ipffn  20837  mplsubrglem  21191  tx1stc  22782  tx2ndc  22783  hmeofn  22889  efmndtmd  23233  qustgplem  23253  nmoffn  23856  rrxmfval  24551  mbfimaopnlem  24800  i1fadd  24840  i1fmul  24841  ex-fpar  28805  smatrcl  31725  txomap  31763  qtophaus  31765  pstmxmet  31826  dya2icoseg  32223  dya2iocrfn  32225  fncvm  33198  cntotbnd  35933  rnghmfn  45400  rhmfn  45428  rnghmsscmap2  45483  rnghmsscmap  45484  rngchomffvalALTV  45505  rngchomrnghmresALTV  45506  rhmsscmap2  45529  rhmsscmap  45530  funcringcsetcALTV2lem4  45549  funcringcsetclem4ALTV  45572  srhmsubc  45586  fldc  45593  fldhmsubc  45594  rhmsubclem1  45596  srhmsubcALTV  45604  fldcALTV  45611  fldhmsubcALTV  45612  rhmsubcALTVlem1  45614  rrx2xpref1o  46016  functhinclem1  46274