Theorem fnmpoi 8019

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

Syntax hints:   = wceq 1547   ∈ wcel 2119  ∀wral 3054  Vcvv 3432   × cxp 5623   Fn wfn 6487   ∈ cmpo 7365

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 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-oprab 7367  df-mpo 7368  df-1st 7938  df-2nd 7939

This theorem is referenced by:  dmmpo  8020  fnoa  8440  fnom  8441  fnoe  8442  fnmap  8777  fnpm  8778  addpqnq  10859  mulpqnq  10862  mpoaddf  11130  mpomulf  11131  elq  12898  cnref1o  12933  ccatfn  14532  qnnen  16178  restfn  17385  prdsdsfn  17426  imasdsfn  17476  imasvscafn  17499  homffn  17657  comfffn  17668  comffn  17669  isoval  17730  cofucl  17853  fnfuc  17913  natffn  17917  catcisolem  18075  estrchomfn  18099  funcestrcsetclem4  18107  funcsetcestrclem4  18122  fnxpc  18140  1stfcl  18161  2ndfcl  18162  prfcl  18167  evlfcl  18186  curf1cl  18192  curfcl  18196  hofcl  18223  yonedalem3  18244  yonedainv  18245  plusffn  18615  mulgfval  19043  mulgfvalALT  19044  mulgfn  19046  gimfn  19234  sylow2blem2  19594  rnghmfn  20417  rhmfn  20477  rnghmsscmap2  20608  rnghmsscmap  20609  rhmsscmap2  20637  rhmsscmap  20638  srhmsubc  20659  rhmsubclem1  20664  fldc  20763  fldhmsubc  20764  scaffn  20880  lmimfn  21023  ipffn  21633  mplsubrglem  21985  tx1stc  23640  tx2ndc  23641  hmeofn  23747  efmndtmd  24091  qustgplem  24111  nmoffn  24701  rrxmfval  25398  mbfimaopnlem  25647  i1fadd  25687  i1fmul  25688  subsfn  28041  ex-fpar  30557  smatrcl  33987  txomap  34025  qtophaus  34027  pstmxmet  34088  dya2icoseg  34468  dya2iocrfn  34470  fncvm  35492  mpomulnzcnf  36534  cntotbnd  38170  grimfn  48377  grlimfn  48477  rngchomffvalALTV  48776  rngchomrnghmresALTV  48777  rhmsubcALTVlem1  48779  funcringcsetcALTV2lem4  48791  funcringcsetclem4ALTV  48814  srhmsubcALTV  48823  fldcALTV  48830  fldhmsubcALTV  48831  rrx2xpref1o  49216  sectfn  49526  discsubclem  49560  oppffn  49621  swapf2fn  49765  fucofn2  49821  fucoppc  49907  functhinclem1  49941  lanfn  50106  ranfn  50107