Theorem mpt2ex 6902

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 2761	. 2 |- A. x e. A B e. _V
4		eqid 2462	. . 3 |- ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> C )
5	4	mpt2exxg 6899	. 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 683	1 |- ( x e. A , y e. B |-> C ) e. _V

Syntax hints:   e. wcel 1898   A.wral 2749   _Vcvv 3057   |-> cmpt2 6322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4531  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-id 4771  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-oprab 6324  df-mpt2 6325  df-1st 6825  df-2nd 6826

This theorem is referenced by:  qexALT  11313  ruclem13  14349  vdwapfval  14976  prdsco  15421  imasvsca  15476  homffval  15650  comfffval  15658  comffval  15659  comfffn  15664  comfeq  15666  oppccofval  15676  monfval  15692  sectffval  15710  invffval  15718  cofu1st  15843  cofu2nd  15845  cofucl  15848  natfval  15906  fuccofval  15919  fucco  15922  coafval  16014  setcco  16033  catchomfval  16048  catccofval  16050  catcco  16051  estrcco  16070  xpcval  16117  xpchomfval  16119  xpccofval  16122  xpcco  16123  1stf1  16132  1stf2  16133  2ndf1  16135  2ndf2  16136  1stfcl  16137  2ndfcl  16138  prf1  16140  prf2fval  16141  prfcl  16143  prf1st  16144  prf2nd  16145  evlf2  16158  evlf1  16160  evlfcl  16162  curf1fval  16164  curf11  16166  curf12  16167  curf1cl  16168  curf2  16169  curfcl  16172  hof1fval  16193  hof2fval  16195  hofcl  16199  yonedalem3  16220  mgmnsgrpex  16720  sgrpnmndex  16721  grpsubfval  16763  mulgfval  16814  symgplusg  17085  lsmfval  17345  pj1fval  17399  dvrfval  17967  psrmulr  18663  psrvscafval  18669  evlslem2  18790  mamufval  19465  mvmulfval  19622  isphtpy  22067  pcofval  22096  q1pval  23160  r1pval  23163  motplusg  24643  midf  24874  ismidb  24876  ttgval  24961  ebtwntg  25068  ecgrtg  25069  elntg  25070  vsfval  26310  dipfval  26394  smatfval  28672  lmatval  28690  qqhval  28829  dya2iocuni  29155  sxbrsigalem5  29160  sitmval  29232  signswplusg  29494  mclsrcl  30249  mclsval  30251  ldualfvs  32748  paddfval  33408  tgrpopr  34360  erngfplus  34415  erngfmul  34418  erngfplus-rN  34423  erngfmul-rN  34426  dvafvadd  34627  dvafvsca  34629  dvaabl  34638  dvhfvadd  34705  dvhfvsca  34714  djafvalN  34748  djhfval  35011  hlhilip  35565  mendplusgfval  36097  mendmulrfval  36099  mendvscafval  36102  hoidmvval  38506  cznrng  40326  cznnring  40327  rngchomfvalALTV  40355  rngccofvalALTV  40358  rngccoALTV  40359  ringchomfvalALTV  40418  ringccofvalALTV  40421  ringccoALTV  40422