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 17	1 |- ( ph -> `' A = `' B )

Syntax hints:   -> wi 4   = wceq 1446   `'ccnv 4836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-in 3413  df-ss 3420  df-br 4406  df-opab 4465  df-cnv 4845

This theorem is referenced by:  cnvsng  5325  opswap  5326  cores2  5351  nvocnv  6185  2ndval2  6816  2nd1st  6843  cnvf1olem  6899  fparlem3  6903  fparlem4  6904  brtpos2  6984  dftpos4  6997  tpostpos  6998  tposf12  7003  xpcomco  7667  infeq123d  8002  cantnffval2  8205  cnfcomlem  8209  fseqenlem2  8461  dfac12lem1  8578  dfac12r  8581  fpwwe2cbv  9060  fpwwe2lem2  9062  fpwwe2lem6  9065  fpwwe2lem9  9068  fpwwecbv  9074  fpwwelem  9075  funcnvs2  13011  funcnvs3  13012  relexpcnv  13110  fsumcnv  13846  fprodcnv  14049  bitsf1ocnv  14430  vdwpc  14942  imasval  15423  imasvalOLD  15424  xpsfval  15485  xpsval  15490  monfval  15649  ismon  15650  monpropd  15654  isepi  15657  invffval  15675  invfval  15676  dfiso2  15689  isofn  15692  oppcinv  15697  isfth  15831  catcisolem  16013  oduval  16388  oduleval  16389  gsumvalx  16525  grpinvcnv  16734  grplactcnv  16766  eqglact  16880  gsumcom2  17619  isunit  17897  issrng  18090  znval  19118  znle2  19136  evpmss  19166  psgnevpmb  19167  ptbasfi  20608  ptval2  20628  ptrescn  20666  xkoptsub  20681  qtopval  20722  txswaphmeolem  20831  xpstopnlem2  20838  ptcmpg  21084  tgplacthmeo  21130  trust  21256  prdsxmslem2  21556  metuval  21576  nghmfval  21739  isnghm  21740  nghmfvalOLD  21757  isnghmOLD  21758  pi1xfrcnv  22100  ismbf1  22594  ismbf  22598  mbfconst  22603  mbfres2  22613  cncombf  22626  deg1val  23057  fta1glem2  23129  fta1g  23130  fta1b  23132  dgrval  23194  dgrlem  23195  coe11  23219  fta1lem  23272  vieta1lem2  23276  ispth  25310  1pthonlem1  25331  constr2spthlem1  25336  2pthlem1  25337  constr2pth  25343  constr3pthlem2  25396  f1o3d  28241  fimacnvinrn  28247  xppreima2  28261  ofpreima  28280  fcnvgreu  28287  fpwrelmapffslem  28329  ordtrest2NEW  28741  qqhval  28790  indf1ofs  28859  esum2dlem  28925  mbfmcst  29093  omssubadd  29140  omssubaddOLD  29144  sitgfval  29186  eulerpartlemgf  29224  orvcval  29302  cvmliftmolem1  30016  cvmliftlem5  30024  cvmliftlem15  30033  cvmlift2lem9a  30038  cvmlift2lem9  30046  ismfs  30199  mthmval  30225  wsuceq123  30509  cnambfre  32001  itg2addnclem2  32006  ftc1anclem1  32029  ftc1anclem6  32034  cdlemg1finvtrlemN  34154  tendoicbv  34372  tendoi  34373  tendoi2  34374  tendoicl  34375  docaffvalN  34701  docafvalN  34702  dihmeetlem1N  34870  dihglblem5apreN  34871  diophrw  35613  rmxfval  35764  rmyfval  35765  aomclem8  35931  cnvtrclfv  36328  frege131d  36368  isPth  39699  2pthdlem1  39755  2spthd  39764  usgra2pthspth  39769