Theorem mpt2ex 7136

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

Hypotheses

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

Assertion

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

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

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

Proof of Theorem mpt2ex

Step	Hyp	Ref	Expression
1		mpt2ex.1	. 2 ⊢ 𝐴 ∈ V
2		mpt2ex.2	. . 3 ⊢ 𝐵 ∈ V
3	2	rgenw 2908	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 ∈ V
4		eqid 2610	. . 3 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
5	4	mpt2exxg 7133	. 2 ⊢ ((𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ V) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V)
6	1, 3, 5	mp2an 704	1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V

Syntax hints:   ∈ wcel 1977  ∀wral 2896  Vcvv 3173   ↦ cmpt2 6551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-oprab 6553  df-mpt2 6554  df-1st 7059  df-2nd 7060

This theorem is referenced by:  qexALT  11679  ruclem13  14810  vdwapfval  15513  prdsco  15951  imasvsca  16003  homffval  16173  comfffval  16181  comffval  16182  comfffn  16187  comfeq  16189  oppccofval  16199  monfval  16215  sectffval  16233  invffval  16241  cofu1st  16366  cofu2nd  16368  cofucl  16371  natfval  16429  fuccofval  16442  fucco  16445  coafval  16537  setcco  16556  catchomfval  16571  catccofval  16573  catcco  16574  estrcco  16593  xpcval  16640  xpchomfval  16642  xpccofval  16645  xpcco  16646  1stf1  16655  1stf2  16656  2ndf1  16658  2ndf2  16659  1stfcl  16660  2ndfcl  16661  prf1  16663  prf2fval  16664  prfcl  16666  prf1st  16667  prf2nd  16668  evlf2  16681  evlf1  16683  evlfcl  16685  curf1fval  16687  curf11  16689  curf12  16690  curf1cl  16691  curf2  16692  curfcl  16695  hof1fval  16716  hof2fval  16718  hofcl  16722  yonedalem3  16743  mgmnsgrpex  17241  sgrpnmndex  17242  grpsubfval  17287  mulgfval  17365  symgplusg  17632  lsmfval  17876  pj1fval  17930  dvrfval  18507  psrmulr  19205  psrvscafval  19211  evlslem2  19333  mamufval  20010  mvmulfval  20167  isphtpy  22588  pcofval  22618  q1pval  23717  r1pval  23720  motplusg  25237  midf  25468  ismidb  25470  ttgval  25555  ebtwntg  25662  ecgrtg  25663  elntg  25664  vsfval  26872  dipfval  26941  smatfval  29189  lmatval  29207  qqhval  29346  dya2iocuni  29672  sxbrsigalem5  29677  sitmval  29738  signswplusg  29958  mclsrcl  30712  mclsval  30714  ldualfvs  33441  paddfval  34101  tgrpopr  35053  erngfplus  35108  erngfmul  35111  erngfplus-rN  35116  erngfmul-rN  35119  dvafvadd  35320  dvafvsca  35322  dvaabl  35331  dvhfvadd  35398  dvhfvsca  35407  djafvalN  35441  djhfval  35704  hlhilip  36258  mendplusgfval  36774  mendmulrfval  36776  mendvscafval  36779  hoidmvval  39467  wwlksnon  41049  wspthsnon  41050  cznrng  41747  cznnring  41748  rngchomfvalALTV  41776  rngccofvalALTV  41779  rngccoALTV  41780  ringchomfvalALTV  41839  ringccofvalALTV  41842  ringccoALTV  41843