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

Theorem cnveqi 5831
Description: Equality inference for converse relation. (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 5830 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
31, 2ax-mp 5 1 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  ccnv 5633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3446  df-in 3918  df-ss 3928  df-br 5107  df-opab 5169  df-cnv 5642
This theorem is referenced by:  mptcnv  6093  cnvin  6098  cnvxp  6110  xp0  6111  imainrect  6134  cnvcnv  6145  cnvrescnv  6148  mptpreima  6191  co01  6214  coi2  6216  funcnvpr  6564  funcnvtp  6565  fcoi1  6717  f1oprswap  6829  f1ocnvd  7605  f1iun  7877  cnvoprab  7993  fparlem3  8047  fparlem4  8048  tz7.48-2  8389  mapsncnv  8834  sbthlem8  9037  1sdomOLD  9196  cnvepnep  9549  infxpenc2  9963  compsscnv  10312  zorn2lem4  10440  funcnvs1  14807  fsumcom2  15664  fprodcom2  15872  fthoppc  17815  oduval  18182  oduleval  18183  pjdm  21129  qtopres  23065  xkocnv  23181  ustneism  23591  mbfres  25024  dflog2  25932  dfrelog  25937  dvlog  26022  efopnlem2  26028  axcontlem2  27956  2trld  28925  0pth  29111  1pthdlem1  29121  1trld  29128  3trld  29158  ex-cnv  29423  cnvadj  30876  cnvprop  31657  gtiso  31661  padct  31683  cnvoprabOLD  31684  f1od2  31685  ordtcnvNEW  32558  ordtrest2NEW  32561  mbfmcst  32916  0rrv  33108  ballotlemrinv  33190  mthmpps  34233  pprodcnveq  34514  br1cnvres  36775  brcnvrabga  36849  dfxrn2  36884  xrninxp  36900  prjspeclsp  40993  cytpval  41579  resnonrel  41952  cononrel1  41954  cononrel2  41955  cnvtrrel  42030  clsneicnv  42465  neicvgnvo  42475
  Copyright terms: Public domain W3C validator