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

Theorem mpteq12dv 4477
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 4476 1  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  C  |->  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    e. wcel 1758    |-> cmpt 4457
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-ral 2803  df-opab 4458  df-mpt 4459
This theorem is referenced by:  mpteq12i  4483  offval  6436  offval3  6680  cantnffval  7979  cnfcomlem  8042  cnfcomlemOLD  8050  fseqenlem1  8304  dfac12lem1  8422  dfac12r  8425  ackbij2lem2  8519  ackbij2lem3  8520  r1om  8523  ccatfval  12390  swrdval  12430  revval  12517  odzval  13980  vdwpc  14158  restval  14483  prdsval  14511  imasval  14567  divsval  14598  mrcfval  14664  cidfval  14732  monfval  14789  ismon  14790  isepi  14797  idfuval  14904  resfval  14920  resfval2  14921  fucval  14986  homafval  15015  idafval  15043  prfval  15127  prf2fval  15129  curfval  15151  curfpropd  15161  hofval  15180  hof2fval  15183  yonedalem3a  15202  yonedalem4a  15203  yonedalem4c  15205  yonedainv  15209  lubfval  15266  glbfval  15279  ipoval  15442  grpinvfval  15694  grpinvpropd  15719  cntzfval  15956  pmtrfval  16074  psgnfval  16124  odfval  16156  sylow1lem2  16218  sylow1lem4  16220  sylow2blem1  16239  sylow3lem1  16246  sylow3lem2  16247  sylow3lem3  16248  sylow3lem6  16251  pj1fval  16311  vrgpfval  16383  gsum2dlem2  16583  gsum2dOLD  16585  gsum2d2  16587  dprdval  16606  dprdvalOLD  16608  dprd2dlem2  16660  dprd2dlem1  16661  dprd2da  16662  dprd2d2  16664  dpjfval  16675  srgbinom  16765  staffval  17054  lspfval  17176  lsppropd  17221  sraval  17379  aspval  17521  asclfval  17527  ressascl  17536  psrval  17551  psrass1lem  17569  psrmulval  17579  mvrfval  17616  opsrval  17679  mpfrcl  17727  evlsval  17728  coe1mul2  17845  evls1fval  17878  evl1fval  17886  isphl  18181  ocvfval  18215  pjfval  18255  uvcfval  18333  mamufval  18407  mvmulfval  18479  marepvfval  18502  submafval  18516  mdetfval  18523  madufval  18574  minmar1fval  18583  ntrfval  18759  clsfval  18760  neifval  18834  lpfval  18873  ordtval  18924  ordtbas2  18926  ordtcnv  18936  ordtrest  18937  ordtrest2  18939  cnpfval  18969  kqval  19430  fmval  19647  fmf  19649  flffval  19693  fcfval  19737  cnextval  19764  tsmsval2  19831  nmfval  20312  nmpropd  20317  nmpropd2  20318  subgnm  20350  tngnm  20368  nmofval  20424  pi1xfrcnv  20760  iscph  20820  tchval  20864  limcfval  21479  dvfval  21504  eldv  21505  mdegfval  21663  mdegmullem  21681  mdegpropd  21687  coe1mul3  21703  ig1pval  21776  taylfval  21956  mirval  23201  vdgrfval  23716  grpoinvfval  23862  nmoofval  24313  eigvalfval  25452  ressnm  26256  ordtprsval  26492  ordtprsuni  26493  ordtcnvNEW  26494  ordtrestNEW  26495  ordtrest2NEW  26497  xrhval  26588  indv  26613  ofcfval  26684  ofcfval3  26688  omsval  26851  sitgval  26861  issibf  26862  sitgfval  26870  signstfv  27107  cvmliftlem5  27321  cvmliftlem15  27330  tailfval  28740  hbtlem1  29626  hbtlem7  29628  rgspnval  29672  cytpval  29724  ovmpt3rab1  30308  ply1mulgsumlem3  30999  ply1mulgsumlem4  31000  ply1mulgsum  31001  cply1mul  31004  lincval  31061  mat2pmatfval  31198  decpmatmullem  31244  decpmatmulsumfsupp  31246  pm2mpval  31267  pm2mpmhmlem1  31290  pm2mpmhmlem2  31291  cpmatfval  31300  lsatset  32958  lkrfval  33055  pmapfval  33723  pclfvalN  33856  polfvalN  33871  watfvalN  33959  ldilfset  34075  ltrnfset  34084  dilfsetN  34119  trnfsetN  34122  trlfset  34127  trlset  34128  tgrpfset  34711  tendofset  34725  erngfset  34766  erngset  34767  erngfset-rN  34774  erngset-rN  34775  dvafset  34971  diaffval  34998  diafval  34999  dvhfset  35048  docaffvalN  35089  docafvalN  35090  djaffvalN  35101  dibffval  35108  dibfval  35109  dicffval  35142  dicfval  35143  dihffval  35198  dochffval  35317  dochfval  35318  djhffval  35364  lcdfval  35556  mapdffval  35594  mapdfval  35595  hvmapffval  35726  hvmapfval  35727  hdmap1ffval  35764  hdmap1fval  35765  hdmapffval  35797  hdmapfval  35798  hgmapffval  35856  hgmapfval  35857  hlhilset  35905
  Copyright terms: Public domain W3C validator