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

Theorem cnveqi 5435
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 5434 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
31, 2ax-mp 5 1 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1631  ccnv 5248
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-in 3730  df-ss 3737  df-br 4787  df-opab 4847  df-cnv 5257
This theorem is referenced by:  mptcnv  5675  cnvin  5681  cnvxp  5692  xp0  5693  imainrect  5716  cnvcnv  5727  cnvcnvOLD  5728  mptpreima  5772  co01  5794  coi2  5796  funcnvpr  6091  funcnvtp  6092  fcoi1  6218  f1oprswap  6321  f1ocnvd  7031  fun11iun  7273  cnvoprab  7379  fparlem3  7430  fparlem4  7431  tz7.48-2  7690  mapsncnv  8058  sbthlem8  8233  1sdom  8319  cnvepnep  8667  infxpenc2  9045  compsscnv  9395  zorn2lem4  9523  funcnvs1  13866  fsumcom2  14713  fprodcom2  14921  strlemor1OLD  16177  xpsc  16425  fthoppc  16790  oduval  17338  oduleval  17339  pjdm  20268  qtopres  21722  xkocnv  21838  ustneism  22247  mbfres  23631  dflog2  24528  dfrelog  24533  dvlog  24618  efopnlem2  24624  axcontlem2  26066  2trld  27085  0pth  27305  1pthdlem1  27315  1trld  27322  3trld  27352  ex-cnv  27636  cnvadj  29091  gtiso  29818  padct  29837  cnvoprabOLD  29838  f1od2  29839  ordtcnvNEW  30306  ordtrest2NEW  30309  mbfmcst  30661  0rrv  30853  ballotlemrinv  30935  mthmpps  31817  pprodcnveq  32327  dfxrn2  34480  xrninxp  34492  cytpval  38313  resnonrel  38424  cononrel1  38426  cononrel2  38427  cnvtrrel  38488  clsneicnv  38929  neicvgnvo  38939
  Copyright terms: Public domain W3C validator