Theorem cnveqi 5125

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

Syntax hints:   = wceq 1370   `'ccnv 4950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-in 3446  df-ss 3453  df-br 4404  df-opab 4462  df-cnv 4959

This theorem is referenced by:  mptcnv  5350  cnvin  5355  cnvxp  5366  xp0  5367  imainrect  5390  cnvcnv  5401  mptpreima  5442  co01  5463  coi2  5465  fcoi1  5696  f1oprswap  5791  f1ocnvd  6422  fun11iun  6650  fparlem3  6787  fparlem4  6788  tz7.48-2  7010  mapsncnv  7372  sbthlem8  7541  1sdom  7629  infxpenc2  8302  infxpenc2OLD  8306  compsscnv  8654  zorn2lem4  8782  fsumcom2  13362  fsumrev  13367  strlemor1  14387  xpsc  14617  fthoppc  14955  oduval  15422  oduleval  15423  dprdfidOLD  16639  pjdm  18260  qtopres  19406  pt1hmeo  19514  xkocnv  19522  ustneism  19933  mbfres  21258  dflog2  22148  dfrelog  22153  dvlog  22232  efopnlem2  22238  axcontlem2  23383  0pth  23641  1pthonlem1  23660  constr2spthlem1  23665  2pthlem1  23666  constr3pthlem2  23714  ex-cnv  23816  cnvadj  25468  gtiso  26167  cnvoprab  26194  f1od2  26195  ordtcnvNEW  26515  ordtrest2NEW  26518  mbfmcst  26838  0rrv  26998  ballotlemrinv  27080  fprodshft  27651  fprodrev  27652  fprodcom2  27659  pprodcnveq  28078  cytpval  29745