Theorem cnveqd 5169

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

Syntax hints:   -> wi 4   = wceq 1374   `'ccnv 4991

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-in 3476  df-ss 3483  df-br 4441  df-opab 4499  df-cnv 5000

This theorem is referenced by:  cnvsng  5485  opswap  5486  cores2  5511  nvocnv  6166  suppssof1OLD  6534  2ndval2  6792  2nd1st  6819  cnvf1olem  6871  fparlem3  6875  fparlem4  6876  brtpos2  6951  dftpos4  6964  tpostpos  6965  tposf12  6970  xpcomco  7597  cantnffval2  8103  cantnfvalOLD  8106  cantnffval2OLD  8125  cnfcomlem  8132  cnfcomlemOLD  8140  fseqenlem2  8395  dfac12lem1  8512  dfac12r  8515  fpwwe2cbv  8997  fpwwe2lem2  8999  fpwwe2lem6  9002  fpwwe2lem9  9005  fpwwecbv  9011  fpwwelem  9012  fsumcnv  13537  bitsf1ocnv  13942  vdwpc  14346  imasval  14755  xpsfval  14811  xpsval  14816  monfval  14977  ismon  14978  monpropd  14982  isepi  14985  invffval  15002  invfval  15003  oppcinv  15020  isfth  15130  catcisolem  15280  oduval  15606  oduleval  15607  gsumvalx  15808  grpinvcnv  15900  grplactcnv  15932  eqglact  16040  gsumval3OLD  16692  gsumcom2  16787  isunit  17083  issrng  17275  rrgsuppOLD  17704  psrbagaddclOLD  17785  evlslem4OLD  17937  evlslem6OLD  17946  coe1sfiOLD  18017  znval  18332  znle2  18352  evpmss  18382  psgnevpmb  18383  ptbasfi  19810  ptval2  19830  ptrescn  19868  xkoptsub  19883  qtopval  19924  txswaphmeolem  20033  xpstopnlem2  20040  ptcmpg  20285  tgplacthmeo  20330  trust  20460  prdsxmslem2  20760  metuvalOLD  20780  metuval  20781  nghmfval  20957  isnghm  20958  pi1xfrcnv  21285  ismbf1  21761  ismbf  21765  mbfconst  21770  mbfres2  21780  cncombf  21793  deg1val  22224  deg1valOLD  22225  fta1glem2  22295  fta1g  22296  fta1b  22298  dgrval  22353  dgrlem  22354  coe11  22377  fta1lem  22430  vieta1lem2  22434  ispth  24232  1pthonlem1  24253  constr2spthlem1  24258  2pthlem1  24259  constr2pth  24265  constr3pthlem2  24318  f1o3d  27130  fimacnvinrn  27134  xppreima2  27146  ofpreima  27165  fcnvgreu  27172  fpwrelmapffslem  27213  ordtrest2NEW  27527  qqhval  27577  indf1ofs  27665  mbfmcst  27856  sitgfval  27909  eulerpartlemgf  27944  orvcval  28022  cvmliftmolem1  28352  cvmliftlem5  28360  cvmliftlem15  28369  cvmlift2lem9a  28374  cvmlift2lem9  28382  relexpcnv  28517  relexprel  28518  fprodcnv  28676  wsuceq123  28933  cnambfre  29627  itg2addnclem2  29631  ftc1anclem1  29654  ftc1anclem6  29659  diophrw  30283  rmxfval  30431  rmyfval  30432  aomclem8  30600  usgra2pthspth  31775  cdlemg1finvtrlemN  35246  tendoicbv  35464  tendoi  35465  tendoi2  35466  tendoicl  35467  docaffvalN  35793  docafvalN  35794  dihmeetlem1N  35962  dihglblem5apreN  35963