Theorem mpoex 8020

Description: If the domain of an operation given by maps-to notation is a set, the operation is a set. (Contributed by Mario Carneiro, 20-Dec-2013.)

Hypotheses

Ref	Expression
mpoex.1	⊢ 𝐴 ∈ V
mpoex.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
mpoex	⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V

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

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

Proof of Theorem mpoex

Step	Hyp	Ref	Expression
1		mpoex.1	. 2 ⊢ 𝐴 ∈ V
2		mpoex.2	. . 3 ⊢ 𝐵 ∈ V
3	2	rgenw 3052	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 ∈ V
4		eqid 2733	. . 3 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
5	4	mpoexxg 8016	. 2 ⊢ ((𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ V) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V)
6	1, 3, 5	mp2an 692	1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V

Syntax hints:   ∈ wcel 2113  ∀wral 3048  Vcvv 3437   ∈ cmpo 7357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-oprab 7359  df-mpo 7360  df-1st 7930  df-2nd 7931

This theorem is referenced by:  mptmpoopabbrdOLD  8022  qexALT  12868  ruclem13  16158  vdwapfval  16890  prdsco  17379  imasvsca  17432  homffval  17604  comfffval  17612  comffval  17613  comfffn  17618  comfeq  17620  oppccofval  17630  monfval  17647  sectffval  17665  invffval  17673  cofu1st  17798  cofu2nd  17800  cofucl  17803  natfval  17864  fuccofval  17877  fucco  17880  coafval  17979  setcco  17998  catchomfval  18017  catccofval  18019  catcco  18020  estrcco  18044  xpcval  18091  xpchomfval  18093  xpccofval  18096  xpcco  18097  1stf1  18106  1stf2  18107  2ndf1  18109  2ndf2  18110  1stfcl  18111  2ndfcl  18112  prf1  18114  prf2fval  18115  prfcl  18117  prf1st  18118  prf2nd  18119  evlf2  18132  evlf1  18134  evlfcl  18136  curf1fval  18138  curf11  18140  curf12  18141  curf1cl  18142  curf2  18143  curfcl  18146  hof1fval  18167  hof2fval  18169  hofcl  18173  yonedalem3  18194  efmndplusg  18796  mgmnsgrpex  18847  sgrpnmndex  18848  grpsubfvalALT  18905  mulgfvalALT  18991  symgvalstruct  19317  lsmfval  19558  pj1fval  19614  dvrfval  20329  psrmulr  21889  psrvscafval  21895  evlslem2  22025  mamufval  22327  mvmulfval  22477  isphtpy  24927  pcofval  24957  q1pval  26107  r1pval  26110  mulsproplem9  28083  motplusg  28540  midf  28774  ismidb  28776  ttgval  28873  ebtwntg  28981  ecgrtg  28982  elntg  28983  wwlksnon  29850  wspthsnon  29851  clwwlknonmpo  30090  vsfval  30634  dipfval  30703  idlsrgmulr  33516  smatfval  33880  lmatval  33898  qqhval  34057  dya2iocuni  34368  sxbrsigalem5  34373  sitmval  34434  signswplusg  34640  reprval  34695  mclsrcl  35677  mclsval  35679  ldualfvs  39308  paddfval  39969  tgrpopr  40919  erngfplus  40974  erngfmul  40977  erngfplus-rN  40982  erngfmul-rN  40985  dvafvadd  41186  dvafvsca  41188  dvaabl  41196  dvhfvadd  41263  dvhfvsca  41272  djafvalN  41306  djhfval  41569  hlhilip  42120  mendplusgfval  43338  mendmulrfval  43340  mendvscafval  43343  mnringmulrd  44380  mnringmulrcld  44385  hoidmvval  46737  cznrng  48423  cznnring  48424  rngchomfvalALTV  48429  rngccofvalALTV  48432  rngccoALTV  48433  ringchomfvalALTV  48463  ringccofvalALTV  48466  ringccoALTV  48467  rrx2xpreen  48881  lines  48893  spheres  48908  funcf2lem2  49243  upfval  49337  swapfelvv  49424  swapf2fvala  49425  swapf1vala  49427  tposcurf1  49460  diag1f1lem  49467  fucoelvv  49481  fucofn2  49485  fucofvalne  49486  fuco112  49490  fuco111  49491  fuco21  49497  prcofelvv  49541  reldmprcof1  49542  reldmprcof2  49543  prcof1  49549  prcof2a  49550  prcof2  49551  functhinclem1  49605  thincciso  49614  functermc2  49670  incat  49762  setc1onsubc  49763  lanfn  49770  ranfn  49771  lanfval  49774  ranfval  49775