Theorem cnveqi 5009

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 5008	. 2 |- ( A = B -> `' A = `' B )
3	1, 2	ax-mp 5	1 |- `' A = `' B

Syntax hints:   = wceq 1369   `'ccnv 4834

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-in 3330  df-ss 3337  df-br 4288  df-opab 4346  df-cnv 4843

This theorem is referenced by:  mptcnv  5234  cnvin  5239  cnvxp  5250  xp0  5251  imainrect  5274  cnvcnv  5285  mptpreima  5326  co01  5347  coi2  5349  fcoi1  5580  f1oprswap  5675  f1ocnvd  6304  fun11iun  6532  fparlem3  6669  fparlem4  6670  tz7.48-2  6889  mapsncnv  7251  sbthlem8  7420  1sdom  7507  infxpenc2  8180  infxpenc2OLD  8184  compsscnv  8532  zorn2lem4  8660  fsumcom2  13233  fsumrev  13238  strlemor1  14257  xpsc  14487  fthoppc  14825  oduval  15292  oduleval  15293  dprdfidOLD  16502  pjdm  18107  qtopres  19246  pt1hmeo  19354  xkocnv  19362  ustneism  19773  mbfres  21097  dflog2  21987  dfrelog  21992  dvlog  22071  efopnlem2  22077  axcontlem2  23162  0pth  23420  1pthonlem1  23439  constr2spthlem1  23444  2pthlem1  23445  constr3pthlem2  23493  ex-cnv  23595  cnvadj  25247  gtiso  25947  cnvoprab  25974  f1od2  25975  ordtcnvNEW  26302  ordtrest2NEW  26305  mbfmcst  26626  0rrv  26786  ballotlemrinv  26868  fprodshft  27438  fprodrev  27439  fprodcom2  27446  pprodcnveq  27865  cytpval  29530