Theorem mpt2ex 6850

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 2815	. 2 |- A. x e. A B e. _V
4		eqid 2454	. . 3 |- ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> C )
5	4	mpt2exxg 6847	. 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 670	1 |- ( x e. A , y e. B |-> C ) e. _V

Syntax hints:   e. wcel 1823   A.wral 2804   _Vcvv 3106   |-> cmpt2 6272

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-rep 4550  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-reu 2811  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-oprab 6274  df-mpt2 6275  df-1st 6773  df-2nd 6774

This theorem is referenced by:  qexALT  11198  ruclem13  14059  vdwapfval  14573  prdsco  14957  imasvsca  15009  homffval  15178  comfffval  15186  comffval  15187  comfffn  15192  comfeq  15194  oppccofval  15204  monfval  15220  sectffval  15238  invffval  15246  cofu1st  15371  cofu2nd  15373  cofucl  15376  natfval  15434  fuccofval  15447  fucco  15450  coafval  15542  setcco  15561  catchomfval  15576  catccofval  15578  catcco  15579  estrcco  15598  xpcval  15645  xpchomfval  15647  xpccofval  15650  xpcco  15651  1stf1  15660  1stf2  15661  2ndf1  15663  2ndf2  15664  1stfcl  15665  2ndfcl  15666  prf1  15668  prf2fval  15669  prfcl  15671  prf1st  15672  prf2nd  15673  evlf2  15686  evlf1  15688  evlfcl  15690  curf1fval  15692  curf11  15694  curf12  15695  curf1cl  15696  curf2  15697  curfcl  15700  hof1fval  15721  hof2fval  15723  hofcl  15727  yonedalem3  15748  mgmnsgrpex  16248  sgrpnmndex  16249  grpsubfval  16291  mulgfval  16342  symgplusg  16613  lsmfval  16857  pj1fval  16911  dvrfval  17528  psrmulr  18232  psrvscafval  18238  evlslem2  18375  mamufval  19054  mvmulfval  19211  isphtpy  21647  pcofval  21676  q1pval  22720  r1pval  22723  motplusg  24130  midf  24343  ismidb  24345  ttgval  24380  ebtwntg  24487  ecgrtg  24488  elntg  24489  vsfval  25726  dipfval  25810  qqhval  28189  dya2iocuni  28491  sxbrsigalem5  28496  sitmval  28554  signswplusg  28776  mclsrcl  29185  mclsval  29187  mendplusgfval  31375  mendmulrfval  31377  mendvscafval  31380  cznrng  33017  cznnring  33018  rngchomfvalALTV  33046  rngccofvalALTV  33049  rngccoALTV  33050  ringchomfvalALTV  33109  ringccofvalALTV  33112  ringccoALTV  33113  ldualfvs  35258  paddfval  35918  tgrpopr  36870  erngfplus  36925  erngfmul  36928  erngfplus-rN  36933  erngfmul-rN  36936  dvafvadd  37137  dvafvsca  37139  dvaabl  37148  dvhfvadd  37215  dvhfvsca  37224  djafvalN  37258  djhfval  37521  hlhilip  38075