Theorem cnveqd 5013

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 5011	. 2 |- ( A = B -> `' A = `' B )
3	1, 2	syl 16	1 |- ( ph -> `' A = `' B )

Syntax hints:   -> wi 4   = wceq 1369   `'ccnv 4837

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-in 3333  df-ss 3340  df-br 4291  df-opab 4349  df-cnv 4846

This theorem is referenced by:  cnvsng  5323  opswap  5324  cores2  5348  nvocnv  5986  suppssof1OLD  6337  2ndval2  6593  2nd1st  6617  cnvf1olem  6668  fparlem3  6672  fparlem4  6673  brtpos2  6749  dftpos4  6762  tpostpos  6763  tposf12  6768  xpcomco  7399  cantnffval2  7901  cantnfvalOLD  7904  cantnffval2OLD  7923  cnfcomlem  7930  cnfcomlemOLD  7938  fseqenlem2  8193  dfac12lem1  8310  dfac12r  8313  fpwwe2cbv  8795  fpwwe2lem2  8797  fpwwe2lem6  8800  fpwwe2lem9  8803  fpwwecbv  8809  fpwwelem  8810  fsumcnv  13238  bitsf1ocnv  13638  vdwpc  14039  imasval  14447  xpsfval  14503  xpsval  14508  monfval  14669  ismon  14670  monpropd  14674  isepi  14677  invffval  14694  invfval  14695  oppcinv  14712  isfth  14822  catcisolem  14972  oduval  15298  oduleval  15299  gsumvalx  15500  grpinvcnv  15592  grplactcnv  15622  eqglact  15730  gsumval3OLD  16380  gsumcom2  16465  isunit  16747  issrng  16933  rrgsuppOLD  17361  psrbagaddclOLD  17437  evlslem4OLD  17588  evlslem6OLD  17597  coe1sfiOLD  17667  znval  17964  znle2  17984  evpmss  18014  psgnevpmb  18015  ptbasfi  19152  ptval2  19172  ptrescn  19210  xkoptsub  19225  qtopval  19266  txswaphmeolem  19375  xpstopnlem2  19382  ptcmpg  19627  tgplacthmeo  19672  trust  19802  prdsxmslem2  20102  metuvalOLD  20122  metuval  20123  nghmfval  20299  isnghm  20300  pi1xfrcnv  20627  ismbf1  21102  ismbf  21106  mbfconst  21111  mbfres2  21121  cncombf  21134  deg1val  21565  deg1valOLD  21566  fta1glem2  21636  fta1g  21637  fta1b  21639  dgrval  21694  dgrlem  21695  coe11  21718  fta1lem  21771  vieta1lem2  21775  ispth  23465  1pthonlem1  23486  constr2spthlem1  23491  2pthlem1  23492  constr2pth  23498  constr3pthlem2  23540  f1o3d  25946  fimacnvinrn  25950  xppreima2  25963  ofpreima  25982  fcnvgreu  25989  fpwrelmapffslem  26030  ordtrest2NEW  26351  qqhval  26401  indf1ofs  26480  mbfmcst  26672  sitgfval  26725  eulerpartlemgf  26760  orvcval  26838  cvmliftmolem1  27168  cvmliftlem5  27176  cvmliftlem15  27185  cvmlift2lem9a  27190  cvmlift2lem9  27198  relexpcnv  27333  relexprel  27334  fprodcnv  27492  wsuceq123  27749  cnambfre  28437  itg2addnclem2  28441  ftc1anclem1  28464  ftc1anclem6  28469  diophrw  29094  rmxfval  29242  rmyfval  29243  aomclem8  29411  usgra2pthspth  30292  cdlemg1finvtrlemN  34216  tendoicbv  34434  tendoi  34435  tendoi2  34436  tendoicl  34437  docaffvalN  34763  docafvalN  34764  dihmeetlem1N  34932  dihglblem5apreN  34933