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

Theorem cnveqi 5039
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 5038 . 2  |-  ( A  =  B  ->  `' A  =  `' B
)
31, 2ax-mp 8 1  |-  `' A  =  `' B
Colors of variables: wff set class
Syntax hints:    = wceq 1652   `'ccnv 4869
This theorem is referenced by:  cnvin  5271  cnvxp  5282  xp0  5283  imainrect  5304  cnvcnv  5315  mptpreima  5355  co01  5376  coi2  5378  fcoi1  5609  fun11iun  5687  f1oprswap  5709  f1ocnvd  6285  fparlem3  6440  fparlem4  6441  tz7.48-2  6691  abianfp  6708  mapsncnv  7052  sbthlem8  7216  1sdom  7303  infxpenc2  7895  compsscnv  8243  zorn2lem4  8371  fsumcom2  12550  fsumrev  12554  fsumshft  12555  strlemor1  13548  xpsc  13774  fthoppc  14112  oduval  14549  oduleval  14550  dprdfid  15567  evlslem2  16560  pjdm  16926  qtopres  17722  pt1hmeo  17830  xkocnv  17838  ustneism  18245  mbfres  19528  dflog2  20450  dfrelog  20455  dvlog  20534  efopnlem2  20540  0pth  21562  1pthonlem1  21581  constr2spthlem1  21586  2pthlem1  21587  constr3pthlem2  21635  ex-cnv  21737  cnvadj  23387  mptcnv  24037  gtiso  24080  mbfmcst  24601  0rrv  24701  ballotlemrinv  24783  fprodshft  25292  fprodrev  25293  fprodcom2  25300  pprodcnveq  25720  axcontlem2  25896  cytpval  27496
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-or 360  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-nfc 2560  df-in 3319  df-ss 3326  df-br 4205  df-opab 4259  df-cnv 4878
  Copyright terms: Public domain W3C validator