Theorem mpoex 8078

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 3085	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 ∈ V
4		eqid 2765	. . 3 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
5	4	mpoexxg 8074	. 2 ⊢ ((𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ V) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V)
6	1, 3, 5	mp2an 705	1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V

This proof depends on syntax axioms:   ∈ wcel 2146  ∀wral 3081  Vcvv 3457   ∈ cmpo 7418

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-oprab 7420  df-mpo 7421  df-1st 7988  df-2nd 7989

This theorem is used by:  qexALT  12999  ruclem13  16315  vdwapfval  17048  prdsco  17538  imasvsca  17591  homffval  17763  comfffval  17771  comffval  17772  comfffn  17777  comfeq  17779  oppccofval  17789  monfval  17806  sectffval  17824  invffval  17832  cofu1st  17957  cofu2nd  17959  cofucl  17962  natfval  18023  fuccofval  18036  fucco  18039  coafval  18138  setcco  18157  catchomfval  18176  catccofval  18178  catcco  18179  estrcco  18203  xpcval  18250  xpchomfval  18252  xpccofval  18255  xpcco  18256  1stf1  18265  1stf2  18266  2ndf1  18268  2ndf2  18269  1stfcl  18270  2ndfcl  18271  prf1  18273  prf2fval  18274  prfcl  18276  prf1st  18277  prf2nd  18278  evlf2  18291  evlf1  18293  evlfcl  18295  curf1fval  18297  curf11  18299  curf12  18300  curf1cl  18301  curf2  18302  curfcl  18305  hof1fval  18326  hof2fval  18328  hofcl  18332  yonedalem3  18353  efmndplusg  18962  mgmnsgrpex  19016  sgrpnmndex  19017  grpsubfvalALT  19074  mulgfvalALT  19159  symgvalstruct  19490  lsmfval  19731  pj1fval  19787  dvrfval  20509  psrmulr  22121  psrvscafval  22127  evlslem2  22259  mamufval  22578  mvmulfval  22728  isphtpy  25169  pcofval  25198  q1pval  26341  r1pval  26344  mulsproplem9  28346  motplusg  28840  midf  29114  ismidb  29116  ttgval  29253  ebtwntg  29361  ecgrtg  29362  elntg  29363  wwlksnon  30229  wspthsnon  30230  clwwlknonmpo  30469  vsfval  31014  dipfval  31083  idlsrgmulr  33820  smatfval  34208  lmatval  34226  qqhval  34385  dya2iocuni  34697  sxbrsigalem5  34702  sitmval  34763  signswplusg  34966  reprval  35021  mclsrcl  36066  mclsval  36068  ldualfvs  39943  paddfval  40604  tgrpopr  41554  erngfplus  41609  erngfmul  41612  erngfplus-rN  41617  erngfmul-rN  41620  dvafvadd  41821  dvafvsca  41823  dvaabl  41831  dvhfvadd  41898  dvhfvsca  41907  djafvalN  41941  djhfval  42204  hlhilip  42755  mendplusgfval  43941  mendmulrfval  43943  mendvscafval  43946  mnringmulrd  44980  mnringmulrcld  44985  hoidmvval  47324  cznrng  49059  cznnring  49060  rngchomfvalALTV  49065  rngccofvalALTV  49068  rngccoALTV  49069  ringchomfvalALTV  49099  ringccofvalALTV  49102  ringccoALTV  49103  rrx2xpreen  49532  lines  49544  spheres  49559  funcf2lem2  49893  upfval  49987  swapfelvv  50074  swapf2fvala  50075  swapf1vala  50077  tposcurf1  50110  diag1f1lem  50117  fucoelvv  50131  fucofn2  50135  fucofvalne  50136  fuco112  50140  fuco111  50141  fuco21  50147  prcofelvv  50191  reldmprcof1  50192  reldmprcof2  50193  prcof1  50199  prcof2a  50200  prcof2  50201  functhinclem1  50255  thincciso  50264  functermc2  50320  incat  50412  setc1onsubc  50413  lanfn  50420  ranfn  50421  lanfval  50424  ranfval  50425  crosspdot0i  50678