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

Theorem cnveqi 5465
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 5464 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
31, 2ax-mp 5 1 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1652  ccnv 5276
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-in 3739  df-ss 3746  df-br 4810  df-opab 4872  df-cnv 5285
This theorem is referenced by:  mptcnv  5717  cnvin  5723  cnvxp  5734  xp0  5735  imainrect  5758  cnvcnv  5769  cnvcnvOLD  5770  mptpreima  5814  co01  5836  coi2  5838  funcnvpr  6129  funcnvtp  6130  fcoi1  6260  f1oprswap  6363  f1ocnvd  7082  fun11iun  7324  cnvoprab  7430  fparlem3  7481  fparlem4  7482  tz7.48-2  7741  mapsncnv  8109  sbthlem8  8284  1sdom  8370  cnvepnep  8718  infxpenc2  9096  compsscnv  9446  zorn2lem4  9574  funcnvs1  13943  fsumcom2  14792  fprodcom2  14999  strlemor1OLD  16243  xpsc  16485  fthoppc  16850  oduval  17398  oduleval  17399  pjdm  20327  qtopres  21781  xkocnv  21897  ustneism  22306  mbfres  23702  dflog2  24598  dfrelog  24603  dvlog  24688  efopnlem2  24694  axcontlem2  26136  2trld  27141  0pth  27361  1pthdlem1  27371  1trld  27378  3trld  27408  ex-cnv  27688  cnvadj  29142  gtiso  29862  padct  29881  cnvoprabOLD  29882  f1od2  29883  ordtcnvNEW  30348  ordtrest2NEW  30351  mbfmcst  30703  0rrv  30896  ballotlemrinv  30978  mthmpps  31859  pprodcnveq  32366  brcnvrabga  34471  dfxrn2  34499  xrninxp  34511  cytpval  38396  resnonrel  38505  cononrel1  38507  cononrel2  38508  cnvtrrel  38569  clsneicnv  39009  neicvgnvo  39019
  Copyright terms: Public domain W3C validator