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

Theorem cnveqi 4856
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 4855 . 2  |-  ( A  =  B  ->  `' A  =  `' B
)
31, 2ax-mp 8 1  |-  `' A  =  `' B
Colors of variables: wff set class
Syntax hints:    = wceq 1623   `'ccnv 4688
This theorem is referenced by:  cnvin  5088  cnvxp  5097  xp0  5098  imainrect  5119  cnvcnv  5126  mptpreima  5166  co01  5187  coi2  5189  fcoi1  5415  fun11iun  5493  f1oprswap  5515  f1ocnvd  6066  fparlem3  6220  fparlem4  6221  tz7.48-2  6454  abianfp  6471  mapsncnv  6814  sbthlem8  6978  1sdom  7065  infxpenc2  7649  compsscnv  7997  zorn2lem4  8126  fsumcom2  12237  fsumrev  12241  fsumshft  12242  strlemor1  13235  xpsc  13459  fthoppc  13797  oduval  14234  oduleval  14235  dprdfid  15252  evlslem2  16249  pjdm  16607  qtopres  17389  pt1hmeo  17497  xkocnv  17505  mbfres  18999  dflog2  19918  dfrelog  19923  dvlog  19998  efopnlem2  20004  ex-cnv  20824  cnvadj  22472  mptcnv  23027  ballotlemrinv  23092  gtiso  23241  mbfmcst  23564  0rrv  23654  pprodcnveq  24423  axcontlem2  24593  trinv  25395  cytpval  27528
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-in 3159  df-ss 3166  df-br 4024  df-opab 4078  df-cnv 4697
  Copyright terms: Public domain W3C validator