MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpt2ex Unicode version

Theorem mpt2ex 6198
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
StepHypRef Expression
1 mpt2ex.1 . 2  |-  A  e. 
_V
2 mpt2ex.2 . . 3  |-  B  e. 
_V
32rgenw 2610 . 2  |-  A. x  e.  A  B  e.  _V
4 eqid 2283 . . 3  |-  ( x  e.  A ,  y  e.  B  |->  C )  =  ( x  e.  A ,  y  e.  B  |->  C )
54mpt2exxg 6195 . 2  |-  ( ( A  e.  _V  /\  A. x  e.  A  B  e.  _V )  ->  (
x  e.  A , 
y  e.  B  |->  C )  e.  _V )
61, 3, 5mp2an 653 1  |-  ( x  e.  A ,  y  e.  B  |->  C )  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1684   A.wral 2543   _Vcvv 2788    e. cmpt2 5860
This theorem is referenced by:  qexALT  10331  ruclem13  12520  vdwapfval  13018  prdsco  13367  imasvsca  13423  homffval  13594  comfffval  13601  comffval  13602  comfffn  13607  comfeq  13609  oppccofval  13619  monfval  13635  sectffval  13653  invffval  13660  cofu1st  13757  cofu2nd  13759  cofucl  13762  natfval  13820  fuccofval  13833  fucco  13836  coafval  13896  setcco  13915  catchomfval  13930  catccofval  13932  catcco  13933  fnxpc  13950  xpcval  13951  xpchomfval  13953  xpccofval  13956  xpcco  13957  1stf1  13966  1stf2  13967  2ndf1  13969  2ndf2  13970  1stfcl  13971  2ndfcl  13972  prf1  13974  prf2fval  13975  prfcl  13977  prf1st  13978  prf2nd  13979  evlf2  13992  evlf1  13994  evlfcl  13996  curf1fval  13998  curf11  14000  curf12  14001  curf1cl  14002  curf2  14003  curfcl  14006  hof1fval  14027  hof2fval  14029  hofcl  14033  yonedalem3  14054  joinfval  14121  meetfval  14128  grpsubfval  14524  mulgfval  14568  symgplusg  14776  lsmfval  14949  pj1fval  15003  dvrfval  15466  psrmulr  16129  psrvscafval  16135  isphtpy  18479  pcofval  18508  q1pval  19539  r1pval  19542  vsfval  21191  dipfval  21275  dya2iocrfn  23580  dya2iocct  23581  dya2iocrrnval  23582  isaddrv  25646  issubcv  25670  ismulcv  25681  isdivcv2  25693  ishoma  25787  isrocatset  25957  sgplpte21  26132  sgplpte22  26138  isray2  26153  isray  26154  mamufval  27443  mendplusgfval  27493  mendmulrfval  27495  mendvscafval  27498  ldualfvs  29326  paddfval  29986  tgrpopr  30936  erngfplus  30991  erngfmul  30994  erngfplus-rN  30999  erngfmul-rN  31002  dvafvadd  31203  dvafvsca  31205  dvaabl  31214  dvhfvadd  31281  dvhfvsca  31290  djafvalN  31324  djhfval  31587  hlhilip  32141
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123
  Copyright terms: Public domain W3C validator