Theorem cnveqi 5028

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

Syntax hints:   = wceq 1455   `'ccnv 4852

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-in 3423  df-ss 3430  df-br 4417  df-opab 4476  df-cnv 4861

This theorem is referenced by:  mptcnv  5257  cnvin  5262  cnvxp  5273  xp0  5274  imainrect  5297  cnvcnv  5307  mptpreima  5347  co01  5369  coi2  5371  funcnvpr  5658  funcnvtp  5659  fcoi1  5780  f1oprswap  5877  f1ocnvd  6545  fun11iun  6780  fparlem3  6925  fparlem4  6926  tz7.48-2  7185  mapsncnv  7544  sbthlem8  7715  1sdom  7801  infxpenc2  8479  compsscnv  8827  zorn2lem4  8955  funcnvs1  13043  fsumcom2  13884  fprodcom2  14087  strlemor1  15266  xpsc  15512  fthoppc  15877  oduval  16425  oduleval  16426  pjdm  19319  qtopres  20762  xkocnv  20878  ustneism  21287  mbfres  22649  dflog2  23559  dfrelog  23564  dvlog  23645  efopnlem2  23651  axcontlem2  25044  0pth  25349  1pthonlem1  25368  constr2spthlem1  25373  2pthlem1  25374  constr3pthlem2  25433  ex-cnv  25936  cnvadj  27594  gtiso  28330  padct  28356  cnvoprab  28357  f1od2  28358  ordtcnvNEW  28775  ordtrest2NEW  28778  mbfmcst  29130  0rrv  29333  ballotlemrinv  29415  ballotlemrinvOLD  29453  mthmpps  30269  pprodcnveq  30699  cytpval  36131  resnonrel  36243  cononrel1  36245  cononrel2  36246  cnvtrrel  36307  0pth-av  39841  1pthdlem1  39850  1trld  39857  2trld  39887  3trld  39913