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

Theorem mpteq12dv 4365
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 4364 1  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  C  |->  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756    e. cmpt 4345
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-ral 2715  df-opab 4346  df-mpt 4347
This theorem is referenced by:  mpteq12i  4371  offval  6322  offval3  6566  cantnffval  7861  cnfcomlem  7924  cnfcomlemOLD  7932  fseqenlem1  8186  dfac12lem1  8304  dfac12r  8307  ackbij2lem2  8401  ackbij2lem3  8402  r1om  8405  ccatfval  12265  swrdval  12305  revval  12392  odzval  13855  vdwpc  14033  restval  14357  prdsval  14385  imasval  14441  divsval  14472  mrcfval  14538  cidfval  14606  monfval  14663  ismon  14664  isepi  14671  idfuval  14778  resfval  14794  resfval2  14795  fucval  14860  homafval  14889  idafval  14917  prfval  15001  prf2fval  15003  curfval  15025  curfpropd  15035  hofval  15054  hof2fval  15057  yonedalem3a  15076  yonedalem4a  15077  yonedalem4c  15079  yonedainv  15083  lubfval  15140  glbfval  15153  ipoval  15316  grpinvfval  15567  grpinvpropd  15592  cntzfval  15829  pmtrfval  15947  psgnfval  15997  odfval  16027  sylow1lem2  16089  sylow1lem4  16091  sylow2blem1  16110  sylow3lem1  16117  sylow3lem2  16118  sylow3lem3  16119  sylow3lem6  16122  pj1fval  16182  vrgpfval  16254  gsum2dlem2  16450  gsum2dOLD  16452  gsum2d2  16454  dprdval  16473  dprdvalOLD  16475  dprd2dlem2  16527  dprd2dlem1  16528  dprd2da  16529  dprd2d2  16531  dpjfval  16542  srgbinom  16631  staffval  16910  lspfval  17031  lsppropd  17076  sraval  17234  aspval  17376  asclfval  17382  ressascl  17391  psrval  17406  psrass1lem  17424  psrmulval  17434  mvrfval  17470  opsrval  17531  mpfrcl  17579  evlsval  17580  coe1mul2  17698  evls1fval  17729  evl1fval  17737  isphl  18032  ocvfval  18066  pjfval  18106  uvcfval  18184  mamufval  18258  mvmulfval  18328  marepvfval  18351  submafval  18365  mdetfval  18372  madufval  18418  minmar1fval  18427  ntrfval  18603  clsfval  18604  neifval  18678  lpfval  18717  ordtval  18768  ordtbas2  18770  ordtcnv  18780  ordtrest  18781  ordtrest2  18783  cnpfval  18813  kqval  19274  fmval  19491  fmf  19493  flffval  19537  fcfval  19581  cnextval  19608  tsmsval2  19675  nmfval  20156  nmpropd  20161  nmpropd2  20162  subgnm  20194  tngnm  20212  nmofval  20268  pi1xfrcnv  20604  iscph  20664  tchval  20708  limcfval  21322  dvfval  21347  eldv  21348  mdegfval  21506  mdegmullem  21524  mdegpropd  21530  coe1mul3  21546  ig1pval  21619  taylfval  21799  mirval  23027  vdgrfval  23516  grpoinvfval  23662  nmoofval  24113  eigvalfval  25252  ressnm  26063  ordtprsval  26300  ordtprsuni  26301  ordtcnvNEW  26302  ordtrestNEW  26303  ordtrest2NEW  26305  xrhval  26396  indv  26421  ofcfval  26492  ofcfval3  26496  omsval  26660  sitgval  26670  issibf  26671  sitgfval  26679  signstfv  26916  cvmliftlem5  27130  cvmliftlem15  27139  tailfval  28546  hbtlem1  29432  hbtlem7  29434  rgspnval  29478  cytpval  29530  ovmpt3rab1  30114  lincval  30832  lsatset  32475  lkrfval  32572  pmapfval  33240  pclfvalN  33373  polfvalN  33388  watfvalN  33476  ldilfset  33592  ltrnfset  33601  dilfsetN  33636  trnfsetN  33639  trlfset  33644  trlset  33645  tgrpfset  34228  tendofset  34242  erngfset  34283  erngset  34284  erngfset-rN  34291  erngset-rN  34292  dvafset  34488  diaffval  34515  diafval  34516  dvhfset  34565  docaffvalN  34606  docafvalN  34607  djaffvalN  34618  dibffval  34625  dibfval  34626  dicffval  34659  dicfval  34660  dihffval  34715  dochffval  34834  dochfval  34835  djhffval  34881  lcdfval  35073  mapdffval  35111  mapdfval  35112  hvmapffval  35243  hvmapfval  35244  hdmap1ffval  35281  hdmap1fval  35282  hdmapffval  35314  hdmapfval  35315  hgmapffval  35373  hgmapfval  35374  hlhilset  35422
  Copyright terms: Public domain W3C validator