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

Theorem mpteq12dv 4500
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 4499 1  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  C  |->  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1438    e. wcel 1869    |-> cmpt 4480
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-ral 2781  df-opab 4481  df-mpt 4482
This theorem is referenced by:  mpteq12i  4506  ovmpt3rab1  6537  offval  6550  offval3  6799  cantnffval  8171  cnfcomlem  8207  fseqenlem1  8457  dfac12lem1  8575  dfac12r  8578  ackbij2lem2  8672  ackbij2lem3  8673  r1om  8676  ccatfval  12717  swrdval  12769  revval  12861  odzval  14729  odzvalOLD  14735  vdwpc  14923  restval  15318  prdsval  15346  imasval  15404  imasvalOLD  15405  qusval  15441  mrcfval  15507  cidfval  15575  monfval  15630  ismon  15631  isepi  15638  idfuval  15774  resfval  15790  resfval2  15791  fucval  15856  homafval  15917  idafval  15945  prfval  16077  prf2fval  16079  curfval  16101  curfpropd  16111  hofval  16130  hof2fval  16133  yonedalem3a  16152  yonedalem4a  16153  yonedalem4c  16155  yonedainv  16159  lubfval  16217  glbfval  16230  ipoval  16393  grpinvfval  16697  grpinvpropd  16722  cntzfval  16967  pmtrfval  17084  psgnfval  17134  odfval  17172  odfvalOLD  17175  sylow1lem2  17244  sylow1lem4  17246  sylow2blem1  17265  sylow3lem1  17272  sylow3lem2  17273  sylow3lem3  17274  sylow3lem6  17277  pj1fval  17337  vrgpfval  17409  gsum2dlem2  17596  gsum2d2  17599  dprdval  17628  dprd2dlem2  17666  dprd2dlem1  17667  dprd2da  17668  dprd2d2  17670  dpjfval  17681  srgbinom  17771  staffval  18068  lspfval  18189  lsppropd  18234  sraval  18392  aspval  18545  asclfval  18551  ressascl  18561  psrval  18579  psrass1lem  18594  psrmulval  18603  mvrfval  18637  opsrval  18691  mpfrcl  18734  evlsval  18735  coe1mul2  18855  cply1mul  18880  evls1fval  18901  evl1fval  18909  isphl  19187  ocvfval  19221  pjfval  19261  uvcfval  19334  mamufval  19402  mvmulfval  19559  marepvfval  19582  submafval  19596  mdetfval  19603  madufval  19654  minmar1fval  19663  mat2pmatfval  19739  cpm2mfval  19765  decpmatmullem  19787  decpmatmulsumfsupp  19789  pm2mpval  19811  pm2mpmhmlem1  19834  pm2mpmhmlem2  19835  chpmatfval  19846  ntrfval  20031  clsfval  20032  neifval  20107  lpfval  20146  ordtval  20197  ordtbas2  20199  ordtcnv  20209  ordtrest  20210  ordtrest2  20212  cnpfval  20242  kqval  20733  fmval  20950  fmf  20952  flffval  20996  fcfval  21040  cnextval  21068  tsmsval2  21136  nmfval  21595  nmpropd  21600  nmpropd2  21601  subgnm  21633  tngnm  21651  nmofval  21711  nmofvalOLD  21730  pi1xfrcnv  22080  iscph  22140  tchval  22184  limcfval  22819  dvfval  22844  eldv  22845  mdegfval  23003  mdegmullem  23019  mdegpropd  23025  coe1mul3  23040  ig1pval  23116  ig1pvalOLD  23122  taylfval  23306  ishlg  24639  mirval  24692  ishpg  24793  lmif  24819  islmib  24821  vdgrfval  25615  grpoinvfval  25944  nmoofval  26395  eigvalfval  27542  ressnm  28413  ordtprsval  28726  ordtprsuni  28727  ordtrestNEW  28729  indv  28836  ofcfval  28921  ofcfval3  28925  omsval  29119  omsvalOLD  29123  sitgval  29167  issibf  29168  sitgfval  29176  signstfv  29454  cvmliftlem5  30014  cvmliftlem15  30023  mvrsval  30145  mrsubffval  30147  elmrsubrn  30160  msubffval  30163  mvhfval  30173  msrfval  30177  fwddifval  30928  fwddifnval  30929  tailfval  31027  lsatset  32481  lkrfval  32578  pmapfval  33246  pclfvalN  33379  polfvalN  33394  watfvalN  33482  ldilfset  33598  ltrnfset  33607  dilfsetN  33643  trnfsetN  33646  trlfset  33651  trlset  33652  tgrpfset  34236  tendofset  34250  erngfset  34291  erngset  34292  erngfset-rN  34299  erngset-rN  34300  dvafset  34496  diaffval  34523  diafval  34524  dvhfset  34573  docaffvalN  34614  docafvalN  34615  djaffvalN  34626  dibffval  34633  dibfval  34634  dicffval  34667  dicfval  34668  dihffval  34723  dochffval  34842  dochfval  34843  djhffval  34889  lcdfval  35081  mapdffval  35119  mapdfval  35120  hvmapffval  35251  hvmapfval  35252  hdmap1ffval  35289  hdmap1fval  35290  hdmapffval  35322  hdmapfval  35323  hgmapffval  35381  hgmapfval  35382  hlhilset  35430  hbtlem1  35908  hbtlem7  35910  rgspnval  35960  cytpval  36012  ovnval  38143  ply1mulgsumlem3  39486  ply1mulgsumlem4  39487  ply1mulgsum  39488  lincval  39508  offval0  39609
  Copyright terms: Public domain W3C validator