Theorem cnveqd 5530

Description: Equality deduction for converse relation. (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 5528	. 2 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → ◡𝐴 = ◡𝐵)

Syntax hints:   → wi 4   = wceq 1656  ^◡ccnv 5341

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-in 3805  df-ss 3812  df-br 4874  df-opab 4936  df-cnv 5350

This theorem is referenced by:  opswap  5863  cores2  5889  fimacnvinrn  6597  nvocnv  6792  2ndval2  7446  2nd1st  7475  cnvf1olem  7539  fparlem3  7543  fparlem4  7544  brtpos2  7623  dftpos4  7636  tpostpos  7637  tposf12  7642  xpcomco  8319  infeq123d  8656  cantnffval2  8869  cnfcomlem  8873  fseqenlem2  9161  dfac12lem1  9280  dfac12r  9283  fpwwe2cbv  9767  fpwwe2lem2  9769  fpwwe2lem6  9772  fpwwe2lem9  9775  fpwwecbv  9781  fpwwelem  9782  funcnvs2  14034  funcnvs3  14035  funcnvs4  14036  relexpcnv  14152  fsumcnv  14879  fprodcnv  15086  bitsf1ocnv  15539  vdwpc  16055  imasval  16524  xpsfval  16580  xpsval  16585  monfval  16744  ismon  16745  monpropd  16749  isepi  16752  invffval  16770  invfval  16771  dfiso2  16784  isofn  16787  oppcinv  16792  isfth  16926  catcisolem  17108  oduval  17483  oduleval  17484  gsumvalx  17623  grpinvcnv  17837  grplactcnv  17872  eqglact  17996  gsumcom2  18727  isunit  19011  issrng  19206  znval  20243  znle2  20261  evpmss  20291  psgnevpmb  20292  ptbasfi  21755  ptval2  21775  ptrescn  21813  xkoptsub  21828  qtopval  21869  txswaphmeolem  21978  xpstopnlem2  21985  ptcmpg  22231  tgplacthmeo  22277  trust  22403  prdsxmslem2  22704  metuval  22724  nghmfval  22896  isnghm  22897  pi1xfrcnv  23226  ismbf1  23790  ismbf  23794  mbfconst  23799  mbfres2  23811  cncombf  23824  deg1val  24255  fta1glem2  24325  fta1g  24326  fta1b  24328  dgrval  24383  dgrlem  24384  coe11  24408  fta1lem  24461  vieta1lem2  24465  ispth  27025  uhgrwkspthlem2  27056  usgr2wlkspthlem1  27059  usgr2wlkspthlem2  27060  pthdlem1  27068  2spthd  27270  3spthd  27541  f1o3d  29969  xppreima2  29988  ofpreima  30003  fcnvgreu  30009  fpwrelmapffslem  30044  ordtrest2NEW  30503  qqhval  30552  indf1ofs  30622  esum2dlem  30688  mbfmcst  30855  omssubadd  30896  sitgfval  30937  eulerpartlemgf  30975  orvcval  31054  cvmliftmolem1  31798  cvmliftlem5  31806  cvmliftlem15  31815  cvmlift2lem9a  31820  cvmlift2lem9  31828  ismfs  31981  mthmval  32007  wsuceq123  32287  cnambfre  33994  itg2addnclem2  33998  ftc1anclem1  34021  ftc1anclem6  34026  dfsymrels2  34832  dfsymrel2  34836  cdlemg1finvtrlemN  36643  tendoicbv  36861  tendoi  36862  tendoi2  36863  tendoicl  36864  docaffvalN  37189  docafvalN  37190  dihmeetlem1N  37358  dihglblem5apreN  37359  diophrw  38159  rmxfval  38305  rmyfval  38306  aomclem8  38467  cnvtrclfv  38850  frege131d  38890  dssmapnvod  39147  smfpimioo  41781  smfpimcc  41801  smfsuplem2  41805