Theorem cnveqd 5298

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

Hypothesis

Ref	Expression
cnveqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
cnveqd	⊢ (𝜑 → ◡𝐴 = ◡𝐵)

Proof of Theorem cnveqd

Step	Hyp	Ref	Expression
1		cnveqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		cnveq 5296	. 2 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → ◡𝐴 = ◡𝐵)

Syntax hints:   → wi 4   = wceq 1483  ^◡ccnv 5113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-in 3581  df-ss 3588  df-br 4654  df-opab 4713  df-cnv 5122

This theorem is referenced by:  cnvsng  5621  opswap  5622  cores2  5648  fimacnvinrn  6348  nvocnv  6537  2ndval2  7186  2nd1st  7213  cnvf1olem  7275  fparlem3  7279  fparlem4  7280  brtpos2  7358  dftpos4  7371  tpostpos  7372  tposf12  7377  xpcomco  8050  infeq123d  8387  cantnffval2  8592  cnfcomlem  8596  fseqenlem2  8848  dfac12lem1  8965  dfac12r  8968  fpwwe2cbv  9452  fpwwe2lem2  9454  fpwwe2lem6  9457  fpwwe2lem9  9460  fpwwecbv  9466  fpwwelem  9467  funcnvs2  13658  funcnvs3  13659  funcnvs4  13660  relexpcnv  13775  fsumcnv  14504  fprodcnv  14713  bitsf1ocnv  15166  vdwpc  15684  imasval  16171  xpsfval  16227  xpsval  16232  monfval  16392  ismon  16393  monpropd  16397  isepi  16400  invffval  16418  invfval  16419  dfiso2  16432  isofn  16435  oppcinv  16440  isfth  16574  catcisolem  16756  oduval  17130  oduleval  17131  gsumvalx  17270  grpinvcnv  17483  grplactcnv  17518  eqglact  17645  gsumcom2  18374  isunit  18657  issrng  18850  znval  19883  znle2  19902  evpmss  19932  psgnevpmb  19933  ptbasfi  21384  ptval2  21404  ptrescn  21442  xkoptsub  21457  qtopval  21498  txswaphmeolem  21607  xpstopnlem2  21614  ptcmpg  21861  tgplacthmeo  21907  trust  22033  prdsxmslem2  22334  metuval  22354  nghmfval  22526  isnghm  22527  pi1xfrcnv  22857  ismbf1  23393  ismbf  23397  mbfconst  23402  mbfres2  23412  cncombf  23425  deg1val  23856  fta1glem2  23926  fta1g  23927  fta1b  23929  dgrval  23984  dgrlem  23985  coe11  24009  fta1lem  24062  vieta1lem2  24066  ispth  26619  uhgrwkspthlem2  26650  usgr2wlkspthlem1  26653  usgr2wlkspthlem2  26654  pthdlem1  26662  2spthd  26837  3spthd  27036  f1o3d  29431  xppreima2  29450  ofpreima  29465  fcnvgreu  29472  fpwrelmapffslem  29507  ordtrest2NEW  29969  qqhval  30018  indf1ofs  30088  esum2dlem  30154  mbfmcst  30321  omssubadd  30362  sitgfval  30403  eulerpartlemgf  30441  orvcval  30519  cvmliftmolem1  31263  cvmliftlem5  31271  cvmliftlem15  31280  cvmlift2lem9a  31285  cvmlift2lem9  31293  ismfs  31446  mthmval  31472  wsuceq123  31760  cnambfre  33458  itg2addnclem2  33462  ftc1anclem1  33485  ftc1anclem6  33490  cdlemg1finvtrlemN  35863  tendoicbv  36081  tendoi  36082  tendoi2  36083  tendoicl  36084  docaffvalN  36410  docafvalN  36411  dihmeetlem1N  36579  dihglblem5apreN  36580  diophrw  37322  rmxfval  37468  rmyfval  37469  aomclem8  37631  cnvtrclfv  38016  frege131d  38056  dssmapnvod  38314  smfpimioo  40994  smfpimcc  41014  smfsuplem2  41018