Theorem cnveqd 5825

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

Syntax hints:   → wi 4   = wceq 1542  ^◡ccnv 5624

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3919  df-br 5100  df-opab 5162  df-cnv 5633

This theorem is referenced by:  opswap  6188  cores2  6219  fimacnvinrn  7018  nvocnv  7230  2ndval2  7954  2nd1st  7985  cnvf1olem  8055  fparlem3  8059  fparlem4  8060  brtpos2  8177  dftpos4  8190  tpostpos  8191  tposf12  8196  xpcomco  9000  infeq123d  9390  cantnffval2  9609  cnfcomlem  9613  fseqenlem2  9940  dfac12lem1  10059  dfac12r  10062  fpwwe2cbv  10546  fpwwe2lem2  10548  fpwwe2lem5  10551  fpwwe2lem8  10554  fpwwecbv  10560  fpwwelem  10561  funcnvs2  14841  funcnvs3  14842  funcnvs4  14843  relexpcnv  14963  fsumcnv  15701  fprodcnv  15911  bitsf1ocnv  16376  vdwpc  16913  imasval  17437  xpsval  17496  monfval  17661  ismon  17662  monpropd  17666  isepi  17669  invffval  17687  invfval  17688  dfiso2  17701  isofn  17704  oppcinv  17709  isfth  17845  catcisolem  18039  oduval  18216  oduleval  18217  gsumvalx  18606  grpinvcnv  18941  grplactcnv  18978  eqglact  19113  gsumcom2  19909  isunit  20314  issrng  20782  znval  21495  znle2  21513  evpmss  21546  psgnevpmb  21547  ptbasfi  23530  ptval2  23550  ptrescn  23588  xkoptsub  23603  qtopval  23644  txswaphmeolem  23753  ptcmpg  24006  tgplacthmeo  24052  trust  24178  prdsxmslem2  24478  metuval  24498  nghmfval  24671  isnghm  24672  pi1xfrcnv  25018  ismbf1  25586  ismbf  25590  mbfconst  25595  mbfres2  25607  cncombf  25620  deg1val  26062  fta1glem2  26135  fta1g  26136  fta1b  26138  dgrval  26194  dgrlem  26195  coe11  26219  fta1lem  26276  vieta1lem2  26280  ispth  29799  dfpth2  29807  uhgrwkspthlem2  29832  usgr2wlkspthlem1  29835  usgr2wlkspthlem2  29836  pthdlem1  29844  2spthd  30019  3spthd  30256  f1o3d  32708  xppreima2  32733  ofpreima  32747  fcnvgreu  32754  mptiffisupp  32775  fpwrelmapffslem  32814  indf1ofs  32951  gsumhashmul  33153  tocycfv  33195  tocycf  33203  cycpm2tr  33205  cycpmconjvlem  33227  evpmval  33231  altgnsg  33235  ply1dg3rt0irred  33669  vieta  33749  irngval  33855  ordtrest2NEW  34093  qqhval  34142  esum2dlem  34262  mbfmcst  34429  omssubadd  34470  sitgfval  34511  eulerpartlemgf  34549  orvcval  34628  pthhashvtx  35335  cvmliftmolem1  35488  cvmliftlem5  35496  cvmliftlem15  35505  cvmlift2lem9a  35510  cvmlift2lem9  35518  ismfs  35756  mthmval  35782  wsuceq123  36019  bj-iminvval2  37412  cnambfre  37882  itg2addnclem2  37886  ftc1anclem1  37907  ftc1anclem6  37912  dfsymrels2  38839  dfsymrel2  38847  cdlemg1finvtrlemN  40914  tendoicbv  41132  tendoi  41133  tendoi2  41134  tendoicl  41135  docaffvalN  41460  docafvalN  41461  dihmeetlem1N  41629  dihglblem5apreN  41630  diophrw  43079  rmxfval  43224  rmyfval  43225  aomclem8  43381  cnvtrclfv  44043  frege131d  44083  dssmapnvod  44339  smfpimioo  47108  smfpimcc  47129  smfsuplem2  47133  upgrimpths  48232  dftpos5  49196  tposideq  49210  invfn  49352  invpropdlem  49360  imaidfu  49432  idfth  49480  idsubc  49482  swapf1a  49591  swapf2a  49593  swapf1  49594  swapf2  49596