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

Theorem cnveqi 4989
Description: Equality inference for converse. (Contributed by NM, 23-Dec-2008.)
Hypothesis
Ref Expression
cnveqi.1  |-  A  =  B
Assertion
Ref Expression
cnveqi  |-  `' A  =  `' B

Proof of Theorem cnveqi
StepHypRef Expression
1 cnveqi.1 . 2  |-  A  =  B
2 cnveq 4988 . 2  |-  ( A  =  B  ->  `' A  =  `' B
)
31, 2ax-mp 8 1  |-  `' A  =  `' B
Colors of variables: wff set class
Syntax hints:    = wceq 1649   `'ccnv 4819
This theorem is referenced by:  cnvin  5221  cnvxp  5232  xp0  5233  imainrect  5254  cnvcnv  5265  mptpreima  5305  co01  5326  coi2  5328  fcoi1  5559  fun11iun  5637  f1oprswap  5659  f1ocnvd  6234  fparlem3  6389  fparlem4  6390  tz7.48-2  6637  abianfp  6654  mapsncnv  6998  sbthlem8  7162  1sdom  7249  infxpenc2  7838  compsscnv  8186  zorn2lem4  8314  fsumcom2  12487  fsumrev  12491  fsumshft  12492  strlemor1  13485  xpsc  13711  fthoppc  14049  oduval  14486  oduleval  14487  dprdfid  15504  evlslem2  16497  pjdm  16859  qtopres  17653  pt1hmeo  17761  xkocnv  17769  ustneism  18176  mbfres  19405  dflog2  20327  dfrelog  20332  dvlog  20411  efopnlem2  20417  0pth  21426  1pthonlem1  21439  2pthonlem1  21449  constr3pthlem2  21493  ex-cnv  21595  cnvadj  23245  mptcnv  23890  gtiso  23931  mbfmcst  24405  0rrv  24490  ballotlemrinv  24572  fprodshft  25081  fprodrev  25082  pprodcnveq  25449  axcontlem2  25620  cytpval  27199
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-in 3272  df-ss 3279  df-br 4156  df-opab 4210  df-cnv 4828
  Copyright terms: Public domain W3C validator