Theorem cnveqd 5710

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 5708	. 2 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → ◡𝐴 = ◡𝐵)

Syntax hints:   → wi 4   = wceq 1538  ^◡ccnv 5518

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-br 5031  df-opab 5093  df-cnv 5527

This theorem is referenced by:  opswap  6053  cores2  6079  fimacnvinrn  6817  nvocnv  7016  2ndval2  7689  2nd1st  7719  cnvf1olem  7788  fparlem3  7792  fparlem4  7793  brtpos2  7881  dftpos4  7894  tpostpos  7895  tposf12  7900  xpcomco  8590  infeq123d  8929  cantnffval2  9142  cnfcomlem  9146  fseqenlem2  9436  dfac12lem1  9554  dfac12r  9557  fpwwe2cbv  10041  fpwwe2lem2  10043  fpwwe2lem6  10046  fpwwe2lem9  10049  fpwwecbv  10055  fpwwelem  10056  funcnvs2  14266  funcnvs3  14267  funcnvs4  14268  relexpcnv  14386  fsumcnv  15120  fprodcnv  15329  bitsf1ocnv  15783  vdwpc  16306  imasval  16776  xpsval  16835  monfval  16994  ismon  16995  monpropd  16999  isepi  17002  invffval  17020  invfval  17021  dfiso2  17034  isofn  17037  oppcinv  17042  isfth  17176  catcisolem  17358  oduval  17732  oduleval  17733  gsumvalx  17878  grpinvcnv  18159  grplactcnv  18194  eqglact  18323  gsumcom2  19088  isunit  19403  issrng  19614  znval  20227  znle2  20245  evpmss  20275  psgnevpmb  20276  ptbasfi  22186  ptval2  22206  ptrescn  22244  xkoptsub  22259  qtopval  22300  txswaphmeolem  22409  ptcmpg  22662  tgplacthmeo  22708  trust  22835  prdsxmslem2  23136  metuval  23156  nghmfval  23328  isnghm  23329  pi1xfrcnv  23662  ismbf1  24228  ismbf  24232  mbfconst  24237  mbfres2  24249  cncombf  24262  deg1val  24697  fta1glem2  24767  fta1g  24768  fta1b  24770  dgrval  24825  dgrlem  24826  coe11  24850  fta1lem  24903  vieta1lem2  24907  ispth  27512  uhgrwkspthlem2  27543  usgr2wlkspthlem1  27546  usgr2wlkspthlem2  27547  pthdlem1  27555  2spthd  27727  3spthd  27961  f1o3d  30386  xppreima2  30413  ofpreima  30428  fcnvgreu  30436  fpwrelmapffslem  30494  gsumhashmul  30741  tocycfv  30801  tocycf  30809  cycpm2tr  30811  cycpmconjvlem  30833  evpmval  30837  altgnsg  30841  ordtrest2NEW  31276  qqhval  31325  indf1ofs  31395  esum2dlem  31461  mbfmcst  31627  omssubadd  31668  sitgfval  31709  eulerpartlemgf  31747  orvcval  31825  pthhashvtx  32487  cvmliftmolem1  32641  cvmliftlem5  32649  cvmliftlem15  32658  cvmlift2lem9a  32663  cvmlift2lem9  32671  ismfs  32909  mthmval  32935  wsuceq123  33214  bj-iminvval2  34609  cnambfre  35105  itg2addnclem2  35109  ftc1anclem1  35130  ftc1anclem6  35135  dfsymrels2  35941  dfsymrel2  35945  cdlemg1finvtrlemN  37871  tendoicbv  38089  tendoi  38090  tendoi2  38091  tendoicl  38092  docaffvalN  38417  docafvalN  38418  dihmeetlem1N  38586  dihglblem5apreN  38587  diophrw  39700  rmxfval  39845  rmyfval  39846  aomclem8  40005  cnvtrclfv  40425  frege131d  40465  dssmapnvod  40721  smfpimioo  43419  smfpimcc  43439  smfsuplem2  43443