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

Theorem mpteq12dv 4525
Description: An equality inference for the maps to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.)
Hypotheses
Ref Expression
mpteq12dv.1  |-  ( ph  ->  A  =  C )
mpteq12dv.2  |-  ( ph  ->  B  =  D )
Assertion
Ref Expression
mpteq12dv  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  C  |->  D ) )
Distinct variable group:    ph, x
Allowed substitution hints:    A( x)    B( x)    C( x)    D( x)

Proof of Theorem mpteq12dv
StepHypRef Expression
1 mpteq12dv.1 . 2  |-  ( ph  ->  A  =  C )
2 mpteq12dv.2 . . 3  |-  ( ph  ->  B  =  D )
32adantr 465 . 2  |-  ( (
ph  /\  x  e.  A )  ->  B  =  D )
41, 3mpteq12dva 4524 1  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  C  |->  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    e. wcel 1767    |-> cmpt 4505
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-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-ral 2819  df-opab 4506  df-mpt 4507
This theorem is referenced by:  mpteq12i  4531  ovmpt3rab1  6518  offval  6531  offval3  6778  cantnffval  8080  cnfcomlem  8143  cnfcomlemOLD  8151  fseqenlem1  8405  dfac12lem1  8523  dfac12r  8526  ackbij2lem2  8620  ackbij2lem3  8621  r1om  8624  ccatfval  12557  swrdval  12607  revval  12697  odzval  14177  vdwpc  14357  restval  14682  prdsval  14710  imasval  14766  divsval  14797  mrcfval  14863  cidfval  14931  monfval  14988  ismon  14989  isepi  14996  idfuval  15103  resfval  15119  resfval2  15120  fucval  15185  homafval  15214  idafval  15242  prfval  15326  prf2fval  15328  curfval  15350  curfpropd  15360  hofval  15379  hof2fval  15382  yonedalem3a  15401  yonedalem4a  15402  yonedalem4c  15404  yonedainv  15408  lubfval  15465  glbfval  15478  ipoval  15641  grpinvfval  15898  grpinvpropd  15923  cntzfval  16163  pmtrfval  16281  psgnfval  16331  odfval  16363  sylow1lem2  16425  sylow1lem4  16427  sylow2blem1  16446  sylow3lem1  16453  sylow3lem2  16454  sylow3lem3  16455  sylow3lem6  16458  pj1fval  16518  vrgpfval  16590  gsum2dlem2  16801  gsum2dOLD  16803  gsum2d2  16805  dprdval  16837  dprdvalOLD  16839  dprd2dlem2  16891  dprd2dlem1  16892  dprd2da  16893  dprd2d2  16895  dpjfval  16906  srgbinom  16998  staffval  17296  lspfval  17419  lsppropd  17464  sraval  17622  aspval  17776  asclfval  17782  ressascl  17792  psrval  17810  psrass1lem  17828  psrmulval  17838  mvrfval  17875  opsrval  17938  mpfrcl  17986  evlsval  17987  coe1mul2  18109  cply1mul  18134  evls1fval  18155  evl1fval  18163  isphl  18458  ocvfval  18492  pjfval  18532  uvcfval  18610  mamufval  18682  mvmulfval  18839  marepvfval  18862  submafval  18876  mdetfval  18883  madufval  18934  minmar1fval  18943  mat2pmatfval  19019  cpm2mfval  19045  decpmatmullem  19067  decpmatmulsumfsupp  19069  pm2mpval  19091  pm2mpmhmlem1  19114  pm2mpmhmlem2  19115  chpmatfval  19126  ntrfval  19319  clsfval  19320  neifval  19394  lpfval  19433  ordtval  19484  ordtbas2  19486  ordtcnv  19496  ordtrest  19497  ordtrest2  19499  cnpfval  19529  kqval  19990  fmval  20207  fmf  20209  flffval  20253  fcfval  20297  cnextval  20324  tsmsval2  20391  nmfval  20872  nmpropd  20877  nmpropd2  20878  subgnm  20910  tngnm  20928  nmofval  20984  pi1xfrcnv  21320  iscph  21380  tchval  21424  limcfval  22039  dvfval  22064  eldv  22065  mdegfval  22223  mdegmullem  22241  mdegpropd  22247  coe1mul3  22263  ig1pval  22336  taylfval  22516  mirval  23777  lmif  23856  islmib  23858  vdgrfval  24599  grpoinvfval  24930  nmoofval  25381  eigvalfval  26520  ressnm  27329  ordtprsval  27564  ordtprsuni  27565  ordtcnvNEW  27566  ordtrestNEW  27567  ordtrest2NEW  27569  xrhval  27660  indv  27694  ofcfval  27765  ofcfval3  27769  omsval  27932  sitgval  27942  issibf  27943  sitgfval  27951  signstfv  28188  cvmliftlem5  28402  cvmliftlem15  28411  tailfval  29821  hbtlem1  30704  hbtlem7  30706  rgspnval  30750  cytpval  30802  ply1mulgsumlem3  32087  ply1mulgsumlem4  32088  ply1mulgsum  32089  lincval  32109  lsatset  33805  lkrfval  33902  pmapfval  34570  pclfvalN  34703  polfvalN  34718  watfvalN  34806  ldilfset  34922  ltrnfset  34931  dilfsetN  34966  trnfsetN  34969  trlfset  34974  trlset  34975  tgrpfset  35558  tendofset  35572  erngfset  35613  erngset  35614  erngfset-rN  35621  erngset-rN  35622  dvafset  35818  diaffval  35845  diafval  35846  dvhfset  35895  docaffvalN  35936  docafvalN  35937  djaffvalN  35948  dibffval  35955  dibfval  35956  dicffval  35989  dicfval  35990  dihffval  36045  dochffval  36164  dochfval  36165  djhffval  36211  lcdfval  36403  mapdffval  36441  mapdfval  36442  hvmapffval  36573  hvmapfval  36574  hdmap1ffval  36611  hdmap1fval  36612  hdmapffval  36644  hdmapfval  36645  hgmapffval  36703  hgmapfval  36704  hlhilset  36752
  Copyright terms: Public domain W3C validator