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

Theorem mpt2ex 7400
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 𝐴 ∈ V
mpt2ex.2 𝐵 ∈ V
Assertion
Ref Expression
mpt2ex (𝑥𝐴, 𝑦𝐵𝐶) ∈ V
Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥,𝑦)

Proof of Theorem mpt2ex
StepHypRef Expression
1 mpt2ex.1 . 2 𝐴 ∈ V
2 mpt2ex.2 . . 3 𝐵 ∈ V
32rgenw 3073 . 2 𝑥𝐴 𝐵 ∈ V
4 eqid 2771 . . 3 (𝑥𝐴, 𝑦𝐵𝐶) = (𝑥𝐴, 𝑦𝐵𝐶)
54mpt2exxg 7397 . 2 ((𝐴 ∈ V ∧ ∀𝑥𝐴 𝐵 ∈ V) → (𝑥𝐴, 𝑦𝐵𝐶) ∈ V)
61, 3, 5mp2an 672 1 (𝑥𝐴, 𝑦𝐵𝐶) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2145  wral 3061  Vcvv 3351  cmpt2 6797
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7099
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-iun 4657  df-br 4788  df-opab 4848  df-mpt 4865  df-id 5158  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-f1 6035  df-fo 6036  df-f1o 6037  df-fv 6038  df-oprab 6799  df-mpt2 6800  df-1st 7318  df-2nd 7319
This theorem is referenced by:  qexALT  12010  ruclem13  15176  vdwapfval  15881  prdsco  16335  imasvsca  16387  homffval  16556  comfffval  16564  comffval  16565  comfffn  16570  comfeq  16572  oppccofval  16582  monfval  16598  sectffval  16616  invffval  16624  cofu1st  16749  cofu2nd  16751  cofucl  16754  natfval  16812  fuccofval  16825  fucco  16828  coafval  16920  setcco  16939  catchomfval  16954  catccofval  16956  catcco  16957  estrcco  16976  xpcval  17024  xpchomfval  17026  xpccofval  17029  xpcco  17030  1stf1  17039  1stf2  17040  2ndf1  17042  2ndf2  17043  1stfcl  17044  2ndfcl  17045  prf1  17047  prf2fval  17048  prfcl  17050  prf1st  17051  prf2nd  17052  evlf2  17065  evlf1  17067  evlfcl  17069  curf1fval  17071  curf11  17073  curf12  17074  curf1cl  17075  curf2  17076  curfcl  17079  hof1fval  17100  hof2fval  17102  hofcl  17106  yonedalem3  17127  mgmnsgrpex  17625  sgrpnmndex  17626  grpsubfval  17671  mulgfval  17749  symgplusg  18015  lsmfval  18259  pj1fval  18313  dvrfval  18891  psrmulr  19598  psrvscafval  19604  evlslem2  19726  mamufval  20407  mvmulfval  20565  isphtpy  22999  pcofval  23028  q1pval  24132  r1pval  24135  motplusg  25657  midf  25888  ismidb  25890  ttgval  25975  ebtwntg  26082  ecgrtg  26083  elntg  26084  wwlksnon  26979  wspthsnon  26980  clwwlknonmpt2  27260  vsfval  27827  dipfval  27896  smatfval  30200  lmatval  30218  qqhval  30357  dya2iocuni  30684  sxbrsigalem5  30689  sitmval  30750  signswplusg  30971  reprval  31027  mclsrcl  31795  mclsval  31797  ldualfvs  34944  paddfval  35605  tgrpopr  36556  erngfplus  36611  erngfmul  36614  erngfplus-rN  36619  erngfmul-rN  36622  dvafvadd  36823  dvafvsca  36825  dvaabl  36834  dvhfvadd  36901  dvhfvsca  36910  djafvalN  36944  djhfval  37207  hlhilip  37758  mendplusgfval  38281  mendmulrfval  38283  mendvscafval  38286  hoidmvval  41308  cznrng  42480  cznnring  42481  rngchomfvalALTV  42509  rngccofvalALTV  42512  rngccoALTV  42513  ringchomfvalALTV  42572  ringccofvalALTV  42575  ringccoALTV  42576
  Copyright terms: Public domain W3C validator