Theorem mpt2ex 6860

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 2825	. 2 |- A. x e. A B e. _V
4		eqid 2467	. . 3 |- ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> C )
5	4	mpt2exxg 6857	. 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 672	1 |- ( x e. A , y e. B |-> C ) e. _V

Syntax hints:   e. wcel 1767   A.wral 2814   _Vcvv 3113   |-> cmpt2 6286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-oprab 6288  df-mpt2 6289  df-1st 6784  df-2nd 6785

This theorem is referenced by:  qexALT  11197  ruclem13  13836  vdwapfval  14348  prdsco  14723  imasvsca  14775  homffval  14947  comfffval  14954  comffval  14955  comfffn  14960  comfeq  14962  oppccofval  14972  monfval  14988  sectffval  15006  invffval  15013  cofu1st  15110  cofu2nd  15112  cofucl  15115  natfval  15173  fuccofval  15186  fucco  15189  coafval  15249  setcco  15268  catchomfval  15283  catccofval  15285  catcco  15286  xpcval  15304  xpchomfval  15306  xpccofval  15309  xpcco  15310  1stf1  15319  1stf2  15320  2ndf1  15322  2ndf2  15323  1stfcl  15324  2ndfcl  15325  prf1  15327  prf2fval  15328  prfcl  15330  prf1st  15331  prf2nd  15332  evlf2  15345  evlf1  15347  evlfcl  15349  curf1fval  15351  curf11  15353  curf12  15354  curf1cl  15355  curf2  15356  curfcl  15359  hof1fval  15380  hof2fval  15382  hofcl  15386  yonedalem3  15407  grpsubfval  15902  mulgfval  15953  symgplusg  16219  lsmfval  16464  pj1fval  16518  dvrfval  17134  psrmulr  17836  psrvscafval  17842  evlslem2  17979  mamufval  18682  mvmulfval  18839  isphtpy  21244  pcofval  21273  q1pval  22317  r1pval  22320  midf  23847  ismidb  23849  ttgval  23882  ebtwntg  23989  ecgrtg  23990  elntg  23991  vsfval  25232  dipfval  25316  qqhval  27619  dya2iocuni  27922  sxbrsigalem5  27927  sitmval  27958  signswplusg  28180  mendplusgfval  30767  mendmulrfval  30769  mendvscafval  30772  ldualfvs  33951  paddfval  34611  tgrpopr  35561  erngfplus  35616  erngfmul  35619  erngfplus-rN  35624  erngfmul-rN  35627  dvafvadd  35828  dvafvsca  35830  dvaabl  35839  dvhfvadd  35906  dvhfvsca  35915  djafvalN  35949  djhfval  36212  hlhilip  36766