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

Theorem cnveqi 4872
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 4871 . 2  |-  ( A  =  B  ->  `' A  =  `' B
)
31, 2ax-mp 8 1  |-  `' A  =  `' B
Colors of variables: wff set class
Syntax hints:    = wceq 1632   `'ccnv 4704
This theorem is referenced by:  cnvin  5104  cnvxp  5113  xp0  5114  imainrect  5135  cnvcnv  5142  mptpreima  5182  co01  5203  coi2  5205  fcoi1  5431  fun11iun  5509  f1oprswap  5531  f1ocnvd  6082  fparlem3  6236  fparlem4  6237  tz7.48-2  6470  abianfp  6487  mapsncnv  6830  sbthlem8  6994  1sdom  7081  infxpenc2  7665  compsscnv  8013  zorn2lem4  8142  fsumcom2  12253  fsumrev  12257  fsumshft  12258  strlemor1  13251  xpsc  13475  fthoppc  13813  oduval  14250  oduleval  14251  dprdfid  15268  evlslem2  16265  pjdm  16623  qtopres  17405  pt1hmeo  17513  xkocnv  17521  mbfres  19015  dflog2  19934  dfrelog  19939  dvlog  20014  efopnlem2  20020  ex-cnv  20840  cnvadj  22488  mptcnv  23043  ballotlemrinv  23108  gtiso  23256  mbfmcst  23579  0rrv  23669  pprodcnveq  24494  axcontlem2  24665  trinv  25498  cytpval  27631  0pth  28356  constr3pthlem2  28402
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-in 3172  df-ss 3179  df-br 4040  df-opab 4094  df-cnv 4713
  Copyright terms: Public domain W3C validator