Theorem mpt2ex 7247

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 2924	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 ∈ V
4		eqid 2622	. . 3 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
5	4	mpt2exxg 7244	. 2 ⊢ ((𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ V) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V)
6	1, 3, 5	mp2an 708	1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V

Syntax hints:   ∈ wcel 1990  ∀wral 2912  Vcvv 3200   ↦ cmpt2 6652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-oprab 6654  df-mpt2 6655  df-1st 7168  df-2nd 7169

This theorem is referenced by:  qexALT  11803  ruclem13  14971  vdwapfval  15675  prdsco  16128  imasvsca  16180  homffval  16350  comfffval  16358  comffval  16359  comfffn  16364  comfeq  16366  oppccofval  16376  monfval  16392  sectffval  16410  invffval  16418  cofu1st  16543  cofu2nd  16545  cofucl  16548  natfval  16606  fuccofval  16619  fucco  16622  coafval  16714  setcco  16733  catchomfval  16748  catccofval  16750  catcco  16751  estrcco  16770  xpcval  16817  xpchomfval  16819  xpccofval  16822  xpcco  16823  1stf1  16832  1stf2  16833  2ndf1  16835  2ndf2  16836  1stfcl  16837  2ndfcl  16838  prf1  16840  prf2fval  16841  prfcl  16843  prf1st  16844  prf2nd  16845  evlf2  16858  evlf1  16860  evlfcl  16862  curf1fval  16864  curf11  16866  curf12  16867  curf1cl  16868  curf2  16869  curfcl  16872  hof1fval  16893  hof2fval  16895  hofcl  16899  yonedalem3  16920  mgmnsgrpex  17418  sgrpnmndex  17419  grpsubfval  17464  mulgfval  17542  symgplusg  17809  lsmfval  18053  pj1fval  18107  dvrfval  18684  psrmulr  19384  psrvscafval  19390  evlslem2  19512  mamufval  20191  mvmulfval  20348  isphtpy  22780  pcofval  22810  q1pval  23913  r1pval  23916  motplusg  25437  midf  25668  ismidb  25670  ttgval  25755  ebtwntg  25862  ecgrtg  25863  elntg  25864  wwlksnon  26738  wspthsnon  26739  vsfval  27488  dipfval  27557  smatfval  29861  lmatval  29879  qqhval  30018  dya2iocuni  30345  sxbrsigalem5  30350  sitmval  30411  signswplusg  30632  reprval  30688  mclsrcl  31458  mclsval  31460  ldualfvs  34423  paddfval  35083  tgrpopr  36035  erngfplus  36090  erngfmul  36093  erngfplus-rN  36098  erngfmul-rN  36101  dvafvadd  36302  dvafvsca  36304  dvaabl  36313  dvhfvadd  36380  dvhfvsca  36389  djafvalN  36423  djhfval  36686  hlhilip  37240  mendplusgfval  37755  mendmulrfval  37757  mendvscafval  37760  hoidmvval  40791  cznrng  41955  cznnring  41956  rngchomfvalALTV  41984  rngccofvalALTV  41987  rngccoALTV  41988  ringchomfvalALTV  42047  ringccofvalALTV  42050  ringccoALTV  42051