Theorem cnveqi 5183

Description: Equality inference for converse. (Contributed by NM, 23-Dec-2008.)

Hypothesis

Ref	Expression
cnveqi.1	|- A = B

Assertion

Ref	Expression
cnveqi	|- `' A = `' B

Proof of Theorem cnveqi

Step	Hyp	Ref	Expression
1		cnveqi.1	. 2 |- A = B
2		cnveq 5182	. 2 |- ( A = B -> `' A = `' B )
3	1, 2	ax-mp 5	1 |- `' A = `' B

Syntax hints:   = wceq 1379   `'ccnv 5004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-in 3488  df-ss 3495  df-br 4454  df-opab 4512  df-cnv 5013

This theorem is referenced by:  mptcnv  5414  cnvin  5419  cnvxp  5430  xp0  5431  imainrect  5454  cnvcnv  5465  mptpreima  5506  co01  5528  coi2  5530  fcoi1  5765  f1oprswap  5861  f1ocnvd  6519  fun11iun  6755  fparlem3  6897  fparlem4  6898  tz7.48-2  7119  mapsncnv  7477  sbthlem8  7646  1sdom  7734  infxpenc2  8411  infxpenc2OLD  8415  compsscnv  8763  zorn2lem4  8891  fsumcom2  13569  fsumrev  13574  strlemor1  14599  xpsc  14829  fthoppc  15167  oduval  15634  oduleval  15635  dprdfidOLD  16936  pjdm  18607  qtopres  20067  pt1hmeo  20175  xkocnv  20183  ustneism  20594  mbfres  21919  dflog2  22814  dfrelog  22819  dvlog  22898  efopnlem2  22904  axcontlem2  24082  0pth  24386  1pthonlem1  24405  constr2spthlem1  24410  2pthlem1  24411  constr3pthlem2  24470  ex-cnv  24973  cnvadj  26625  gtiso  27333  cnvoprab  27360  f1od2  27361  ordtcnvNEW  27718  ordtrest2NEW  27721  mbfmcst  28046  0rrv  28206  ballotlemrinv  28288  mthmpps  28758  fprodshft  29024  fprodrev  29025  fprodcom2  29032  pprodcnveq  29451  cytpval  31089  cnvtrrel  37148