Theorem fnmpoi 7942

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 3067	. 2 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ V
3		fmpo.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
4	3	fnmpo 7941	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ V → 𝐹 Fn (𝐴 × 𝐵))
5	2, 4	ax-mp 5	1 ⊢ 𝐹 Fn (𝐴 × 𝐵)

Syntax hints:   = wceq 1539   ∈ wcel 2104  ∀wral 3062  Vcvv 3437   × cxp 5598   Fn wfn 6453   ∈ cmpo 7309

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361  ax-un 7620

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ral 3063  df-rex 3072  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-id 5500  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-fv 6466  df-oprab 7311  df-mpo 7312  df-1st 7863  df-2nd 7864

This theorem is referenced by:  dmmpo  7943  fnoa  8369  fnom  8370  fnoe  8371  fnmap  8653  fnpm  8654  addpqnq  10740  mulpqnq  10743  elq  12736  cnref1o  12771  ccatfn  14320  qnnen  15967  restfn  17180  prdsdsfn  17221  imasdsfn  17270  imasvscafn  17293  homffn  17447  comfffn  17458  comffn  17459  isoval  17522  cofucl  17648  fnfuc  17706  natffn  17710  catcisolem  17870  estrchomfn  17896  funcestrcsetclem4  17905  funcsetcestrclem4  17920  fnxpc  17938  1stfcl  17959  2ndfcl  17960  prfcl  17965  evlfcl  17985  curf1cl  17991  curfcl  17995  hofcl  18022  yonedalem3  18043  yonedainv  18044  plusffn  18380  mulgfval  18747  mulgfvalALT  18748  mulgfn  18750  gimfn  18922  sylow2blem2  19271  scaffn  20189  lmimfn  20333  ipffn  20901  mplsubrglem  21255  tx1stc  22846  tx2ndc  22847  hmeofn  22953  efmndtmd  23297  qustgplem  23317  nmoffn  23920  rrxmfval  24615  mbfimaopnlem  24864  i1fadd  24904  i1fmul  24905  ex-fpar  28871  smatrcl  31791  txomap  31829  qtophaus  31831  pstmxmet  31892  dya2icoseg  32289  dya2iocrfn  32291  fncvm  33264  cntotbnd  35998  rnghmfn  45506  rhmfn  45534  rnghmsscmap2  45589  rnghmsscmap  45590  rngchomffvalALTV  45611  rngchomrnghmresALTV  45612  rhmsscmap2  45635  rhmsscmap  45636  funcringcsetcALTV2lem4  45655  funcringcsetclem4ALTV  45678  srhmsubc  45692  fldc  45699  fldhmsubc  45700  rhmsubclem1  45702  srhmsubcALTV  45710  fldcALTV  45717  fldhmsubcALTV  45718  rhmsubcALTVlem1  45720  rrx2xpref1o  46122  functhinclem1  46380