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

Theorem mpteq12dv 4481
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 467 . 2  |-  ( (
ph  /\  x  e.  A )  ->  B  =  D )
41, 3mpteq12dva 4480 1  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  C  |->  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1444    e. wcel 1887    |-> cmpt 4461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-ral 2742  df-opab 4462  df-mpt 4463
This theorem is referenced by:  mpteq12i  4487  ovmpt3rab1  6525  offval  6538  offval3  6787  cantnffval  8168  cnfcomlem  8204  fseqenlem1  8455  dfac12lem1  8573  dfac12r  8576  ackbij2lem2  8670  ackbij2lem3  8671  r1om  8674  ccatfval  12719  swrdval  12773  revval  12865  odzval  14736  odzvalOLD  14742  vdwpc  14930  restval  15325  prdsval  15353  imasval  15411  imasvalOLD  15412  qusval  15448  mrcfval  15514  cidfval  15582  monfval  15637  ismon  15638  isepi  15645  idfuval  15781  resfval  15797  resfval2  15798  fucval  15863  homafval  15924  idafval  15952  prfval  16084  prf2fval  16086  curfval  16108  curfpropd  16118  hofval  16137  hof2fval  16140  yonedalem3a  16159  yonedalem4a  16160  yonedalem4c  16162  yonedainv  16166  lubfval  16224  glbfval  16237  ipoval  16400  grpinvfval  16704  grpinvpropd  16729  cntzfval  16974  pmtrfval  17091  psgnfval  17141  odfval  17179  odfvalOLD  17182  sylow1lem2  17251  sylow1lem4  17253  sylow2blem1  17272  sylow3lem1  17279  sylow3lem2  17280  sylow3lem3  17281  sylow3lem6  17284  pj1fval  17344  vrgpfval  17416  gsum2dlem2  17603  gsum2d2  17606  dprdval  17635  dprd2dlem2  17673  dprd2dlem1  17674  dprd2da  17675  dprd2d2  17677  dpjfval  17688  srgbinom  17778  staffval  18075  lspfval  18196  lsppropd  18241  sraval  18399  aspval  18552  asclfval  18558  ressascl  18568  psrval  18586  psrass1lem  18601  psrmulval  18610  mvrfval  18644  opsrval  18698  mpfrcl  18741  evlsval  18742  coe1mul2  18862  cply1mul  18887  evls1fval  18908  evl1fval  18916  isphl  19195  ocvfval  19229  pjfval  19269  uvcfval  19342  mamufval  19410  mvmulfval  19567  marepvfval  19590  submafval  19604  mdetfval  19611  madufval  19662  minmar1fval  19671  mat2pmatfval  19747  cpm2mfval  19773  decpmatmullem  19795  decpmatmulsumfsupp  19797  pm2mpval  19819  pm2mpmhmlem1  19842  pm2mpmhmlem2  19843  chpmatfval  19854  ntrfval  20039  clsfval  20040  neifval  20115  lpfval  20154  ordtval  20205  ordtbas2  20207  ordtcnv  20217  ordtrest  20218  ordtrest2  20220  cnpfval  20250  kqval  20741  fmval  20958  fmf  20960  flffval  21004  fcfval  21048  cnextval  21076  tsmsval2  21144  nmfval  21603  nmpropd  21608  nmpropd2  21609  subgnm  21641  tngnm  21659  nmofval  21719  nmofvalOLD  21738  pi1xfrcnv  22088  iscph  22148  tchval  22192  limcfval  22827  dvfval  22852  eldv  22853  mdegfval  23011  mdegmullem  23027  mdegpropd  23033  coe1mul3  23048  ig1pval  23124  ig1pvalOLD  23130  taylfval  23314  ishlg  24647  mirval  24700  ishpg  24801  lmif  24827  islmib  24829  vdgrfval  25623  grpoinvfval  25952  nmoofval  26403  eigvalfval  27550  ressnm  28412  ordtprsval  28724  ordtprsuni  28725  ordtrestNEW  28727  indv  28834  ofcfval  28919  ofcfval3  28923  omsval  29117  omsvalOLD  29121  sitgval  29165  issibf  29166  sitgfval  29174  signstfv  29452  cvmliftlem5  30012  cvmliftlem15  30021  mvrsval  30143  mrsubffval  30145  elmrsubrn  30158  msubffval  30161  mvhfval  30171  msrfval  30175  fwddifval  30929  fwddifnval  30930  tailfval  31028  lsatset  32556  lkrfval  32653  pmapfval  33321  pclfvalN  33454  polfvalN  33469  watfvalN  33557  ldilfset  33673  ltrnfset  33682  dilfsetN  33718  trnfsetN  33721  trlfset  33726  trlset  33727  tgrpfset  34311  tendofset  34325  erngfset  34366  erngset  34367  erngfset-rN  34374  erngset-rN  34375  dvafset  34571  diaffval  34598  diafval  34599  dvhfset  34648  docaffvalN  34689  docafvalN  34690  djaffvalN  34701  dibffval  34708  dibfval  34709  dicffval  34742  dicfval  34743  dihffval  34798  dochffval  34917  dochfval  34918  djhffval  34964  lcdfval  35156  mapdffval  35194  mapdfval  35195  hvmapffval  35326  hvmapfval  35327  hdmap1ffval  35364  hdmap1fval  35365  hdmapffval  35397  hdmapfval  35398  hgmapffval  35456  hgmapfval  35457  hlhilset  35505  hbtlem1  35982  hbtlem7  35984  rgspnval  36034  cytpval  36086  ovnval  38362  hspmbllem2  38449  vtxdgfval  39528  ply1mulgsumlem3  40233  ply1mulgsumlem4  40234  ply1mulgsum  40235  lincval  40255  offval0  40356
  Copyright terms: Public domain W3C validator