Theorem cnveqd 5168

Description: Equality deduction for converse. (Contributed by NM, 6-Dec-2013.)

Hypothesis

Ref	Expression
cnveqd.1	|- ( ph -> A = B )

Assertion

Ref	Expression
cnveqd	|- ( ph -> `' A = `' B )

Proof of Theorem cnveqd

Step	Hyp	Ref	Expression
1		cnveqd.1	. 2 |- ( ph -> A = B )
2		cnveq 5166	. 2 |- ( A = B -> `' A = `' B )
3	1, 2	syl 16	1 |- ( ph -> `' A = `' B )

Syntax hints:   -> wi 4   = wceq 1383   `'ccnv 4988

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-in 3468  df-ss 3475  df-br 4438  df-opab 4496  df-cnv 4997

This theorem is referenced by:  cnvsng  5484  opswap  5485  cores2  5510  nvocnv  6172  suppssof1OLD  6544  2ndval2  6803  2nd1st  6830  cnvf1olem  6883  fparlem3  6887  fparlem4  6888  brtpos2  6963  dftpos4  6976  tpostpos  6977  tposf12  6982  xpcomco  7609  cantnffval2  8117  cantnfvalOLD  8120  cantnffval2OLD  8139  cnfcomlem  8146  cnfcomlemOLD  8154  fseqenlem2  8409  dfac12lem1  8526  dfac12r  8529  fpwwe2cbv  9011  fpwwe2lem2  9013  fpwwe2lem6  9016  fpwwe2lem9  9019  fpwwecbv  9025  fpwwelem  9026  fsumcnv  13569  fprodcnv  13768  bitsf1ocnv  14075  vdwpc  14479  imasval  14889  xpsfval  14945  xpsval  14950  monfval  15108  ismon  15109  monpropd  15113  isepi  15116  invffval  15133  invfval  15134  oppcinv  15151  isfth  15261  catcisolem  15411  oduval  15738  oduleval  15739  gsumvalx  15875  grpinvcnv  16084  grplactcnv  16116  eqglact  16230  gsumval3OLD  16886  gsumcom2  16981  isunit  17284  issrng  17477  rrgsuppOLD  17918  psrbagaddclOLD  17999  evlslem4OLD  18151  evlslem6OLD  18160  coe1sfiOLD  18231  znval  18549  znle2  18569  evpmss  18599  psgnevpmb  18600  ptbasfi  20059  ptval2  20079  ptrescn  20117  xkoptsub  20132  qtopval  20173  txswaphmeolem  20282  xpstopnlem2  20289  ptcmpg  20534  tgplacthmeo  20579  trust  20709  prdsxmslem2  21009  metuvalOLD  21029  metuval  21030  nghmfval  21206  isnghm  21207  pi1xfrcnv  21534  ismbf1  22010  ismbf  22014  mbfconst  22019  mbfres2  22029  cncombf  22042  deg1val  22473  deg1valOLD  22474  fta1glem2  22544  fta1g  22545  fta1b  22547  dgrval  22602  dgrlem  22603  coe11  22626  fta1lem  22679  vieta1lem2  22683  ispth  24546  1pthonlem1  24567  constr2spthlem1  24572  2pthlem1  24573  constr2pth  24579  constr3pthlem2  24632  f1o3d  27447  fimacnvinrn  27451  xppreima2  27464  ofpreima  27483  fcnvgreu  27490  fpwrelmapffslem  27531  ordtrest2NEW  27882  qqhval  27932  indf1ofs  28016  mbfmcst  28207  sitgfval  28260  eulerpartlemgf  28295  orvcval  28373  cvmliftmolem1  28703  cvmliftlem5  28711  cvmliftlem15  28720  cvmlift2lem9a  28725  cvmlift2lem9  28733  ismfs  28886  mthmval  28912  relexpcnv  29033  relexprel  29034  wsuceq123  29345  cnambfre  30038  itg2addnclem2  30042  ftc1anclem1  30065  ftc1anclem6  30070  diophrw  30667  rmxfval  30815  rmyfval  30816  aomclem8  30982  usgra2pthspth  32189  cdlemg1finvtrlemN  36041  tendoicbv  36259  tendoi  36260  tendoi2  36261  tendoicl  36262  docaffvalN  36588  docafvalN  36589  dihmeetlem1N  36757  dihglblem5apreN  36758