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

Theorem mpteq12dv 4475
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 4474 1  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  C  |->  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1407    e. wcel 1844    |-> cmpt 4455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-an 371  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-ral 2761  df-opab 4456  df-mpt 4457
This theorem is referenced by:  mpteq12i  4481  ovmpt3rab1  6517  offval  6530  offval3  6780  cantnffval  8114  cnfcomlem  8177  cnfcomlemOLD  8185  fseqenlem1  8439  dfac12lem1  8557  dfac12r  8560  ackbij2lem2  8654  ackbij2lem3  8655  r1om  8658  ccatfval  12648  swrdval  12700  revval  12792  odzval  14529  vdwpc  14709  restval  15043  prdsval  15071  imasval  15127  qusval  15158  mrcfval  15224  cidfval  15292  monfval  15347  ismon  15348  isepi  15355  idfuval  15491  resfval  15507  resfval2  15508  fucval  15573  homafval  15634  idafval  15662  prfval  15794  prf2fval  15796  curfval  15818  curfpropd  15828  hofval  15847  hof2fval  15850  yonedalem3a  15869  yonedalem4a  15870  yonedalem4c  15872  yonedainv  15876  lubfval  15934  glbfval  15947  ipoval  16110  grpinvfval  16414  grpinvpropd  16439  cntzfval  16684  pmtrfval  16801  psgnfval  16851  odfval  16883  sylow1lem2  16945  sylow1lem4  16947  sylow2blem1  16966  sylow3lem1  16973  sylow3lem2  16974  sylow3lem3  16975  sylow3lem6  16978  pj1fval  17038  vrgpfval  17110  gsum2dlem2  17321  gsum2dOLD  17323  gsum2d2  17325  dprdval  17356  dprdvalOLD  17358  dprd2dlem2  17411  dprd2dlem1  17412  dprd2da  17413  dprd2d2  17415  dpjfval  17426  srgbinom  17518  staffval  17818  lspfval  17941  lsppropd  17986  sraval  18144  aspval  18299  asclfval  18305  ressascl  18315  psrval  18333  psrass1lem  18351  psrmulval  18361  mvrfval  18398  opsrval  18461  mpfrcl  18509  evlsval  18510  coe1mul2  18632  cply1mul  18657  evls1fval  18678  evl1fval  18686  isphl  18963  ocvfval  18997  pjfval  19037  uvcfval  19113  mamufval  19181  mvmulfval  19338  marepvfval  19361  submafval  19375  mdetfval  19382  madufval  19433  minmar1fval  19442  mat2pmatfval  19518  cpm2mfval  19544  decpmatmullem  19566  decpmatmulsumfsupp  19568  pm2mpval  19590  pm2mpmhmlem1  19613  pm2mpmhmlem2  19614  chpmatfval  19625  ntrfval  19819  clsfval  19820  neifval  19895  lpfval  19934  ordtval  19985  ordtbas2  19987  ordtcnv  19997  ordtrest  19998  ordtrest2  20000  cnpfval  20030  kqval  20521  fmval  20738  fmf  20740  flffval  20784  fcfval  20828  cnextval  20855  tsmsval2  20922  nmfval  21403  nmpropd  21408  nmpropd2  21409  subgnm  21441  tngnm  21459  nmofval  21515  pi1xfrcnv  21851  iscph  21911  tchval  21955  limcfval  22570  dvfval  22595  eldv  22596  mdegfval  22754  mdegmullem  22772  mdegpropd  22778  coe1mul3  22794  ig1pval  22867  taylfval  23048  mirval  24425  ishpg  24520  lmif  24546  islmib  24548  vdgrfval  25324  grpoinvfval  25653  nmoofval  26104  eigvalfval  27242  ressnm  28104  ordtprsval  28366  ordtprsuni  28367  ordtrestNEW  28369  indv  28473  ofcfval  28558  ofcfval3  28562  omsval  28754  sitgval  28793  issibf  28794  sitgfval  28802  signstfv  29039  cvmliftlem5  29599  cvmliftlem15  29608  mvrsval  29730  mrsubffval  29732  elmrsubrn  29745  msubffval  29748  mvhfval  29758  msrfval  29762  fwddifval  30513  fwddifnval  30514  tailfval  30613  lsatset  32021  lkrfval  32118  pmapfval  32786  pclfvalN  32919  polfvalN  32934  watfvalN  33022  ldilfset  33138  ltrnfset  33147  dilfsetN  33183  trnfsetN  33186  trlfset  33191  trlset  33192  tgrpfset  33776  tendofset  33790  erngfset  33831  erngset  33832  erngfset-rN  33839  erngset-rN  33840  dvafset  34036  diaffval  34063  diafval  34064  dvhfset  34113  docaffvalN  34154  docafvalN  34155  djaffvalN  34166  dibffval  34173  dibfval  34174  dicffval  34207  dicfval  34208  dihffval  34263  dochffval  34382  dochfval  34383  djhffval  34429  lcdfval  34621  mapdffval  34659  mapdfval  34660  hvmapffval  34791  hvmapfval  34792  hdmap1ffval  34829  hdmap1fval  34830  hdmapffval  34862  hdmapfval  34863  hgmapffval  34921  hgmapfval  34922  hlhilset  34970  hbtlem1  35449  hbtlem7  35451  rgspnval  35494  cytpval  35546  ply1mulgsumlem3  38512  ply1mulgsumlem4  38513  ply1mulgsum  38514  lincval  38534  offval0  38635
  Copyright terms: Public domain W3C validator