Theorem fnmpoi 7903

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

Syntax hints:   = wceq 1542   ∈ wcel 2110  ∀wral 3066  Vcvv 3431   × cxp 5588   Fn wfn 6427   ∈ cmpo 7273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356  ax-un 7582

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-iun 4932  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-fv 6440  df-oprab 7275  df-mpo 7276  df-1st 7824  df-2nd 7825

This theorem is referenced by:  dmmpo  7904  fnoa  8323  fnom  8324  fnoe  8325  fnmap  8605  fnpm  8606  addpqnq  10695  mulpqnq  10698  elq  12689  cnref1o  12724  ccatfn  14273  qnnen  15920  restfn  17133  prdsdsfn  17174  imasdsfn  17223  imasvscafn  17246  homffn  17400  comfffn  17411  comffn  17412  isoval  17475  cofucl  17601  fnfuc  17659  natffn  17663  catcisolem  17823  estrchomfn  17849  funcestrcsetclem4  17858  funcsetcestrclem4  17873  fnxpc  17891  1stfcl  17912  2ndfcl  17913  prfcl  17918  evlfcl  17938  curf1cl  17944  curfcl  17948  hofcl  17975  yonedalem3  17996  yonedainv  17997  plusffn  18333  mulgfval  18700  mulgfvalALT  18701  mulgfn  18703  gimfn  18875  sylow2blem2  19224  scaffn  20142  lmimfn  20286  ipffn  20854  mplsubrglem  21208  tx1stc  22799  tx2ndc  22800  hmeofn  22906  efmndtmd  23250  qustgplem  23270  nmoffn  23873  rrxmfval  24568  mbfimaopnlem  24817  i1fadd  24857  i1fmul  24858  ex-fpar  28822  smatrcl  31742  txomap  31780  qtophaus  31782  pstmxmet  31843  dya2icoseg  32240  dya2iocrfn  32242  fncvm  33215  cntotbnd  35950  rnghmfn  45417  rhmfn  45445  rnghmsscmap2  45500  rnghmsscmap  45501  rngchomffvalALTV  45522  rngchomrnghmresALTV  45523  rhmsscmap2  45546  rhmsscmap  45547  funcringcsetcALTV2lem4  45566  funcringcsetclem4ALTV  45589  srhmsubc  45603  fldc  45610  fldhmsubc  45611  rhmsubclem1  45613  srhmsubcALTV  45621  fldcALTV  45628  fldhmsubcALTV  45629  rhmsubcALTVlem1  45631  rrx2xpref1o  46033  functhinclem1  46291