Theorem cnveqi 5297

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

Syntax hints:   = wceq 1483   `'ccnv 5113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-in 3581  df-ss 3588  df-br 4654  df-opab 4713  df-cnv 5122

This theorem is referenced by:  mptcnv  5534  cnvin  5540  cnvxp  5551  xp0  5552  imainrect  5575  cnvcnv  5586  cnvcnvOLD  5587  mptpreima  5628  co01  5650  coi2  5652  funcnvpr  5950  funcnvtp  5951  fcoi1  6078  f1oprswap  6180  f1ocnvd  6884  fun11iun  7126  fparlem3  7279  fparlem4  7280  tz7.48-2  7537  mapsncnv  7904  sbthlem8  8077  1sdom  8163  infxpenc2  8845  compsscnv  9193  zorn2lem4  9321  funcnvs1  13657  fsumcom2  14505  fsumcom2OLD  14506  fprodcom2  14714  fprodcom2OLD  14715  strlemor1OLD  15969  xpsc  16217  fthoppc  16583  oduval  17130  oduleval  17131  pjdm  20051  qtopres  21501  xkocnv  21617  ustneism  22027  mbfres  23411  dflog2  24307  dfrelog  24312  dvlog  24397  efopnlem2  24403  axcontlem2  25845  2trld  26834  0pth  26986  1pthdlem1  26995  1trld  27002  3trld  27032  ex-cnv  27294  cnvadj  28751  gtiso  29478  padct  29497  cnvoprab  29498  f1od2  29499  ordtcnvNEW  29966  ordtrest2NEW  29969  mbfmcst  30321  0rrv  30513  ballotlemrinv  30595  mthmpps  31479  pprodcnveq  31990  cytpval  37787  resnonrel  37898  cononrel1  37900  cononrel2  37901  cnvtrrel  37962  clsneicnv  38403  neicvgnvo  38413