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

Theorem mpteq12dv 4290
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 453 . 2  |-  ( (
ph  /\  x  e.  A )  ->  B  =  D )
41, 3mpteq12dva 4289 1  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  C  |->  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    e. wcel 1726    e. cmpt 4269
This theorem is referenced by:  mpteq12i  4296  offval  6315  offval3  6321  cantnffval  7621  cnfcomlem  7659  fseqenlem1  7910  dfac12lem1  8028  dfac12r  8031  ackbij2lem2  8125  ackbij2lem3  8126  r1om  8129  ccatfval  11747  swrdval  11769  revval  11797  odzval  13182  vdwpc  13353  restval  13659  prdsval  13683  imasval  13742  divsval  13772  mrcfval  13838  cidfval  13906  monfval  13963  ismon  13964  isepi  13971  idfuval  14078  resfval  14094  resfval2  14095  fucval  14160  homafval  14189  idafval  14217  prfval  14301  prf2fval  14303  curfval  14325  curfpropd  14335  hofval  14354  hof2fval  14357  yonedalem3a  14376  yonedalem4a  14377  yonedalem4c  14379  yonedainv  14383  lubfval  14440  glbfval  14445  ipoval  14585  grpinvfval  14848  grpinvpropd  14871  cntzfval  15124  odfval  15176  sylow1lem2  15238  sylow1lem4  15240  sylow2blem1  15259  sylow3lem1  15266  sylow3lem2  15267  sylow3lem3  15268  sylow3lem6  15271  pj1fval  15331  vrgpfval  15403  gsum2d  15551  gsum2d2  15553  dprdval  15566  dprd2dlem2  15603  dprd2dlem1  15604  dprd2da  15605  dprd2d2  15607  dpjfval  15618  staffval  15940  lspfval  16054  lsppropd  16099  sraval  16253  aspval  16392  asclfval  16398  ressascl  16407  psrval  16434  psrass1lem  16447  psrmulval  16455  mvrfval  16489  opsrval  16540  coe1mul2  16667  isphl  16864  ocvfval  16898  pjfval  16938  ntrfval  17093  clsfval  17094  neifval  17168  lpfval  17207  ordtval  17258  ordtbas2  17260  ordtcnv  17270  ordtrest  17271  ordtrest2  17273  cnpfval  17303  kqval  17763  fmval  17980  fmf  17982  flffval  18026  fcfval  18070  cnextval  18097  tsmsval2  18164  nmfval  18641  nmpropd  18646  nmpropd2  18647  subgnm  18679  tngnm  18697  nmofval  18753  pi1xfrcnv  19087  iscph  19138  tchval  19182  limcfval  19764  dvfval  19789  eldv  19790  mpfrcl  19944  evlsval  19945  evl1fval  19952  mdegfval  19990  mdegmullem  20006  mdegpropd  20012  coe1mul3  20027  ig1pval  20100  taylfval  20280  vdgrfval  21671  grpoinvfval  21817  nmoofval  22268  eigvalfval  23405  ressnm  24189  xrhval  24389  indv  24415  ofcfval  24486  ofcfval3  24490  sitgval  24652  issibf  24653  sitgfval  24660  cvmliftlem5  24981  cvmliftlem15  24990  tailfval  26415  uvcfval  27224  hbtlem1  27318  hbtlem7  27320  rgspnval  27364  pmtrfval  27384  psgnfval  27414  mamufval  27434  mdetfval  27478  cytpval  27519  lsatset  29862  lkrfval  29959  pmapfval  30627  pclfvalN  30760  polfvalN  30775  watfvalN  30863  ldilfset  30979  ltrnfset  30988  dilfsetN  31023  trnfsetN  31026  trlfset  31031  trlset  31032  tgrpfset  31615  tendofset  31629  erngfset  31670  erngset  31671  erngfset-rN  31678  erngset-rN  31679  dvafset  31875  diaffval  31902  diafval  31903  dvhfset  31952  docaffvalN  31993  docafvalN  31994  djaffvalN  32005  dibffval  32012  dibfval  32013  dicffval  32046  dicfval  32047  dihffval  32102  dochffval  32221  dochfval  32222  djhffval  32268  lcdfval  32460  mapdffval  32498  mapdfval  32499  hvmapffval  32630  hvmapfval  32631  hdmap1ffval  32668  hdmap1fval  32669  hdmapffval  32701  hdmapfval  32702  hgmapffval  32760  hgmapfval  32761  hlhilset  32809
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-ral 2712  df-opab 4270  df-mpt 4271
  Copyright terms: Public domain W3C validator