Theorem cnveqi 5029

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

Syntax hints:   = wceq 1437   `'ccnv 4853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-in 3449  df-ss 3456  df-br 4427  df-opab 4485  df-cnv 4862

This theorem is referenced by:  mptcnv  5258  cnvin  5263  cnvxp  5274  xp0  5275  imainrect  5298  cnvcnv  5308  mptpreima  5348  co01  5370  coi2  5372  fcoi1  5774  f1oprswap  5870  f1ocnvd  6532  fun11iun  6767  fparlem3  6909  fparlem4  6910  tz7.48-2  7167  mapsncnv  7526  sbthlem8  7695  1sdom  7781  infxpenc2  8451  compsscnv  8799  zorn2lem4  8927  fsumcom2  13813  fprodcom2  14016  strlemor1  15179  xpsc  15414  fthoppc  15779  oduval  16327  oduleval  16328  pjdm  19201  qtopres  20644  xkocnv  20760  ustneism  21169  mbfres  22477  dflog2  23375  dfrelog  23380  dvlog  23461  efopnlem2  23467  axcontlem2  24841  0pth  25145  1pthonlem1  25164  constr2spthlem1  25169  2pthlem1  25170  constr3pthlem2  25229  ex-cnv  25732  cnvadj  27380  gtiso  28121  padct  28150  cnvoprab  28151  f1od2  28152  ordtcnvNEW  28565  ordtrest2NEW  28568  mbfmcst  28920  0rrv  29110  ballotlemrinv  29192  mthmpps  30008  pprodcnveq  30435  cytpval  35785  cnvtrrel  35901