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

Theorem cnveqi 5219
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 5218 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
31, 2ax-mp 5 1 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1475  ccnv 5037
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-in 3547  df-ss 3554  df-br 4584  df-opab 4644  df-cnv 5046
This theorem is referenced by:  mptcnv  5453  cnvin  5459  cnvxp  5470  xp0  5471  imainrect  5494  cnvcnv  5505  mptpreima  5545  co01  5567  coi2  5569  funcnvpr  5864  funcnvtp  5865  fcoi1  5991  f1oprswap  6092  f1ocnvd  6782  fun11iun  7019  fparlem3  7166  fparlem4  7167  tz7.48-2  7424  mapsncnv  7790  sbthlem8  7962  1sdom  8048  infxpenc2  8728  compsscnv  9076  zorn2lem4  9204  funcnvs1  13507  fsumcom2  14347  fsumcom2OLD  14348  fprodcom2  14553  fprodcom2OLD  14554  strlemor1  15796  xpsc  16040  fthoppc  16406  oduval  16953  oduleval  16954  pjdm  19870  qtopres  21311  xkocnv  21427  ustneism  21837  mbfres  23217  dflog2  24111  dfrelog  24116  dvlog  24197  efopnlem2  24203  axcontlem2  25645  0pth  26100  1pthonlem1  26119  constr2spthlem1  26124  2pthlem1  26125  constr3pthlem2  26184  ex-cnv  26686  cnvadj  28135  gtiso  28861  padct  28885  cnvoprab  28886  f1od2  28887  ordtcnvNEW  29294  ordtrest2NEW  29297  mbfmcst  29648  0rrv  29840  ballotlemrinv  29922  mthmpps  30733  pprodcnveq  31160  cytpval  36806  resnonrel  36917  cononrel1  36919  cononrel2  36920  cnvtrrel  36981  clsneicnv  37423  neicvgnvo  37433  2trld  41145  0pth-av  41293  1pthdlem1  41302  1trld  41309  3trld  41339
  Copyright terms: Public domain W3C validator