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

Theorem mpteq12dv 4279
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 452 . 2  |-  ( (
ph  /\  x  e.  A )  ->  B  =  D )
41, 3mpteq12dva 4278 1  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  C  |->  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. wcel 1725    e. cmpt 4258
This theorem is referenced by:  mpteq12i  4285  offval  6303  offval3  6309  cantnffval  7607  cnfcomlem  7645  fseqenlem1  7894  dfac12lem1  8012  dfac12r  8015  ackbij2lem2  8109  ackbij2lem3  8110  r1om  8113  ccatfval  11730  swrdval  11752  revval  11780  odzval  13165  vdwpc  13336  restval  13642  prdsval  13666  imasval  13725  divsval  13755  mrcfval  13821  cidfval  13889  monfval  13946  ismon  13947  isepi  13954  idfuval  14061  resfval  14077  resfval2  14078  fucval  14143  homafval  14172  idafval  14200  prfval  14284  prf2fval  14286  curfval  14308  curfpropd  14318  hofval  14337  hof2fval  14340  yonedalem3a  14359  yonedalem4a  14360  yonedalem4c  14362  yonedainv  14366  lubfval  14423  glbfval  14428  ipoval  14568  grpinvfval  14831  grpinvpropd  14854  cntzfval  15107  odfval  15159  sylow1lem2  15221  sylow1lem4  15223  sylow2blem1  15242  sylow3lem1  15249  sylow3lem2  15250  sylow3lem3  15251  sylow3lem6  15254  pj1fval  15314  vrgpfval  15386  gsum2d  15534  gsum2d2  15536  dprdval  15549  dprd2dlem2  15586  dprd2dlem1  15587  dprd2da  15588  dprd2d2  15590  dpjfval  15601  staffval  15923  lspfval  16037  lsppropd  16082  sraval  16236  aspval  16375  asclfval  16381  ressascl  16390  psrval  16417  psrass1lem  16430  psrmulval  16438  mvrfval  16472  opsrval  16523  coe1mul2  16650  isphl  16847  ocvfval  16881  pjfval  16921  ntrfval  17076  clsfval  17077  neifval  17151  lpfval  17190  ordtval  17241  ordtbas2  17243  ordtcnv  17253  ordtrest  17254  ordtrest2  17256  cnpfval  17286  kqval  17746  fmval  17963  fmf  17965  flffval  18009  fcfval  18053  cnextval  18080  tsmsval2  18147  nmfval  18624  nmpropd  18629  nmpropd2  18630  subgnm  18662  tngnm  18680  nmofval  18736  pi1xfrcnv  19070  iscph  19121  tchval  19165  limcfval  19747  dvfval  19772  eldv  19773  mpfrcl  19927  evlsval  19928  evl1fval  19935  mdegfval  19973  mdegmullem  19989  mdegpropd  19995  coe1mul3  20010  ig1pval  20083  taylfval  20263  vdgrfval  21654  grpoinvfval  21800  nmoofval  22251  eigvalfval  23388  ressnm  24172  xrhval  24372  indv  24398  ofcfval  24469  ofcfval3  24473  sitgval  24635  issibf  24636  sitgfval  24643  cvmliftlem5  24964  cvmliftlem15  24973  tailfval  26338  uvcfval  27148  hbtlem1  27242  hbtlem7  27244  rgspnval  27288  pmtrfval  27308  psgnfval  27338  mamufval  27358  mdetfval  27402  cytpval  27443  shwrd  28120  lsatset  29627  lkrfval  29724  pmapfval  30392  pclfvalN  30525  polfvalN  30540  watfvalN  30628  ldilfset  30744  ltrnfset  30753  dilfsetN  30788  trnfsetN  30791  trlfset  30796  trlset  30797  tgrpfset  31380  tendofset  31394  erngfset  31435  erngset  31436  erngfset-rN  31443  erngset-rN  31444  dvafset  31640  diaffval  31667  diafval  31668  dvhfset  31717  docaffvalN  31758  docafvalN  31759  djaffvalN  31770  dibffval  31777  dibfval  31778  dicffval  31811  dicfval  31812  dihffval  31867  dochffval  31986  dochfval  31987  djhffval  32033  lcdfval  32225  mapdffval  32263  mapdfval  32264  hvmapffval  32395  hvmapfval  32396  hdmap1ffval  32433  hdmap1fval  32434  hdmapffval  32466  hdmapfval  32467  hgmapffval  32525  hgmapfval  32526  hlhilset  32574
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-ral 2702  df-opab 4259  df-mpt 4260
  Copyright terms: Public domain W3C validator