Theorem fnmpoi 8111

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

Syntax hints:   = wceq 1537   ∈ wcel 2108  ∀wral 3067  Vcvv 3488   × cxp 5698   Fn wfn 6568   ∈ cmpo 7450

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-fv 6581  df-oprab 7452  df-mpo 7453  df-1st 8030  df-2nd 8031

This theorem is referenced by:  dmmpo  8112  fnoa  8564  fnom  8565  fnoe  8566  fnmap  8891  fnpm  8892  addpqnq  11007  mulpqnq  11010  mpoaddf  11278  mpomulf  11279  elq  13015  cnref1o  13050  ccatfn  14620  qnnen  16261  restfn  17484  prdsdsfn  17525  imasdsfn  17574  imasvscafn  17597  homffn  17751  comfffn  17762  comffn  17763  isoval  17826  cofucl  17952  fnfuc  18013  natffn  18017  catcisolem  18177  estrchomfn  18203  funcestrcsetclem4  18212  funcsetcestrclem4  18227  fnxpc  18245  1stfcl  18266  2ndfcl  18267  prfcl  18272  evlfcl  18292  curf1cl  18298  curfcl  18302  hofcl  18329  yonedalem3  18350  yonedainv  18351  plusffn  18687  mulgfval  19109  mulgfvalALT  19110  mulgfn  19112  gimfn  19301  sylow2blem2  19663  rnghmfn  20465  rhmfn  20525  rnghmsscmap2  20651  rnghmsscmap  20652  rhmsscmap2  20680  rhmsscmap  20681  srhmsubc  20702  rhmsubclem1  20707  fldc  20807  fldhmsubc  20808  scaffn  20903  lmimfn  21048  ipffn  21692  mplsubrglem  22047  tx1stc  23679  tx2ndc  23680  hmeofn  23786  efmndtmd  24130  qustgplem  24150  nmoffn  24753  rrxmfval  25459  mbfimaopnlem  25709  i1fadd  25749  i1fmul  25750  subsfn  28074  ex-fpar  30494  smatrcl  33742  txomap  33780  qtophaus  33782  pstmxmet  33843  dya2icoseg  34242  dya2iocrfn  34244  fncvm  35225  mpomulnzcnf  36265  cntotbnd  37756  grimfn  47749  grlimfn  47803  rngchomffvalALTV  48001  rngchomrnghmresALTV  48002  rhmsubcALTVlem1  48004  funcringcsetcALTV2lem4  48016  funcringcsetclem4ALTV  48039  srhmsubcALTV  48048  fldcALTV  48055  fldhmsubcALTV  48056  rrx2xpref1o  48452  functhinclem1  48708