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

Theorem cnveqi 5207
Description: Equality inference for converse. (Contributed by NM, 23-Dec-2008.)
Hypothesis
Ref Expression
cnveqi.1 𝐴 = 𝐵
Assertion
Ref Expression
cnveqi 𝐴 = 𝐵

Proof of Theorem cnveqi
StepHypRef Expression
1 cnveqi.1 . 2 𝐴 = 𝐵
2 cnveq 5206 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
31, 2ax-mp 5 1 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  ccnv 5027
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-in 3546  df-ss 3553  df-br 4578  df-opab 4638  df-cnv 5036
This theorem is referenced by:  mptcnv  5440  cnvin  5445  cnvxp  5456  xp0  5457  imainrect  5480  cnvcnv  5491  mptpreima  5531  co01  5553  coi2  5555  funcnvpr  5850  funcnvtp  5851  fcoi1  5976  f1oprswap  6077  f1ocnvd  6759  fun11iun  6996  fparlem3  7143  fparlem4  7144  tz7.48-2  7401  mapsncnv  7767  sbthlem8  7939  1sdom  8025  infxpenc2  8705  compsscnv  9053  zorn2lem4  9181  funcnvs1  13453  fsumcom2  14293  fsumcom2OLD  14294  fprodcom2  14499  fprodcom2OLD  14500  strlemor1  15742  xpsc  15986  fthoppc  16352  oduval  16899  oduleval  16900  pjdm  19812  qtopres  21253  xkocnv  21369  ustneism  21779  mbfres  23134  dflog2  24028  dfrelog  24033  dvlog  24114  efopnlem2  24120  axcontlem2  25563  0pth  25866  1pthonlem1  25885  constr2spthlem1  25890  2pthlem1  25891  constr3pthlem2  25950  ex-cnv  26452  cnvadj  27941  gtiso  28667  padct  28691  cnvoprab  28692  f1od2  28693  ordtcnvNEW  29100  ordtrest2NEW  29103  mbfmcst  29454  0rrv  29646  ballotlemrinv  29728  mthmpps  30539  pprodcnveq  30966  cytpval  36602  resnonrel  36713  cononrel1  36715  cononrel2  36716  cnvtrrel  36777  clsneicnv  37219  neicvgnvo  37229  2trld  41140  0pth-av  41288  1pthdlem1  41297  1trld  41304  3trld  41334
  Copyright terms: Public domain W3C validator