Theorem mpt2ex 6880

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	|- A e. _V
mpt2ex.2	|- B e. _V

Assertion

Ref	Expression
mpt2ex	|- ( x e. A , y e. B |-> C ) e. _V

Distinct variable groups:   x, y, A   y, B

Allowed substitution hints:   B( x)   C( x, y)

Proof of Theorem mpt2ex

Step	Hyp	Ref	Expression
1		mpt2ex.1	. 2 |- A e. _V
2		mpt2ex.2	. . 3 |- B e. _V
3	2	rgenw 2786	. 2 |- A. x e. A B e. _V
4		eqid 2422	. . 3 |- ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> C )
5	4	mpt2exxg 6877	. 2 |- ( ( A e. _V /\ A. x e. A B e. _V ) -> ( x e. A , y e. B |-> C ) e. _V )
6	1, 3, 5	mp2an 676	1 |- ( x e. A , y e. B |-> C ) e. _V

Syntax hints:   e. wcel 1868   A.wral 2775   _Vcvv 3081   |-> cmpt2 6303

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4764  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-oprab 6305  df-mpt2 6306  df-1st 6803  df-2nd 6804

This theorem is referenced by:  qexALT  11279  ruclem13  14279  vdwapfval  14906  prdsco  15351  imasvsca  15406  homffval  15580  comfffval  15588  comffval  15589  comfffn  15594  comfeq  15596  oppccofval  15606  monfval  15622  sectffval  15640  invffval  15648  cofu1st  15773  cofu2nd  15775  cofucl  15778  natfval  15836  fuccofval  15849  fucco  15852  coafval  15944  setcco  15963  catchomfval  15978  catccofval  15980  catcco  15981  estrcco  16000  xpcval  16047  xpchomfval  16049  xpccofval  16052  xpcco  16053  1stf1  16062  1stf2  16063  2ndf1  16065  2ndf2  16066  1stfcl  16067  2ndfcl  16068  prf1  16070  prf2fval  16071  prfcl  16073  prf1st  16074  prf2nd  16075  evlf2  16088  evlf1  16090  evlfcl  16092  curf1fval  16094  curf11  16096  curf12  16097  curf1cl  16098  curf2  16099  curfcl  16102  hof1fval  16123  hof2fval  16125  hofcl  16129  yonedalem3  16150  mgmnsgrpex  16650  sgrpnmndex  16651  grpsubfval  16693  mulgfval  16744  symgplusg  17015  lsmfval  17275  pj1fval  17329  dvrfval  17897  psrmulr  18593  psrvscafval  18599  evlslem2  18720  mamufval  19394  mvmulfval  19551  isphtpy  21996  pcofval  22025  q1pval  23088  r1pval  23091  motplusg  24571  midf  24802  ismidb  24804  ttgval  24889  ebtwntg  24996  ecgrtg  24997  elntg  24998  vsfval  26237  dipfval  26321  smatfval  28614  lmatval  28632  qqhval  28771  dya2iocuni  29098  sxbrsigalem5  29103  sitmval  29175  signswplusg  29437  mclsrcl  30192  mclsval  30194  ldualfvs  32618  paddfval  33278  tgrpopr  34230  erngfplus  34285  erngfmul  34288  erngfplus-rN  34293  erngfmul-rN  34296  dvafvadd  34497  dvafvsca  34499  dvaabl  34508  dvhfvadd  34575  dvhfvsca  34584  djafvalN  34618  djhfval  34881  hlhilip  35435  mendplusgfval  35968  mendmulrfval  35970  mendvscafval  35973  cznrng  39143  cznnring  39144  rngchomfvalALTV  39172  rngccofvalALTV  39175  rngccoALTV  39176  ringchomfvalALTV  39235  ringccofvalALTV  39238  ringccoALTV  39239