Theorem cnveqd 5818

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

Syntax hints:   → wi 4   = wceq 1540  ^◡ccnv 5618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3920  df-br 5093  df-opab 5155  df-cnv 5627

This theorem is referenced by:  opswap  6178  cores2  6208  fimacnvinrn  7005  nvocnv  7218  2ndval2  7942  2nd1st  7973  cnvf1olem  8043  fparlem3  8047  fparlem4  8048  brtpos2  8165  dftpos4  8178  tpostpos  8179  tposf12  8184  xpcomco  8984  infeq123d  9372  cantnffval2  9591  cnfcomlem  9595  fseqenlem2  9919  dfac12lem1  10038  dfac12r  10041  fpwwe2cbv  10524  fpwwe2lem2  10526  fpwwe2lem5  10529  fpwwe2lem8  10532  fpwwecbv  10538  fpwwelem  10539  funcnvs2  14820  funcnvs3  14821  funcnvs4  14822  relexpcnv  14942  fsumcnv  15680  fprodcnv  15890  bitsf1ocnv  16355  vdwpc  16892  imasval  17415  xpsval  17474  monfval  17639  ismon  17640  monpropd  17644  isepi  17647  invffval  17665  invfval  17666  dfiso2  17679  isofn  17682  oppcinv  17687  isfth  17823  catcisolem  18017  oduval  18194  oduleval  18195  gsumvalx  18550  grpinvcnv  18885  grplactcnv  18922  eqglact  19058  gsumcom2  19854  isunit  20258  issrng  20729  znval  21442  znle2  21460  evpmss  21493  psgnevpmb  21494  ptbasfi  23466  ptval2  23486  ptrescn  23524  xkoptsub  23539  qtopval  23580  txswaphmeolem  23689  ptcmpg  23942  tgplacthmeo  23988  trust  24115  prdsxmslem2  24415  metuval  24435  nghmfval  24608  isnghm  24609  pi1xfrcnv  24955  ismbf1  25523  ismbf  25527  mbfconst  25532  mbfres2  25544  cncombf  25557  deg1val  25999  fta1glem2  26072  fta1g  26073  fta1b  26075  dgrval  26131  dgrlem  26132  coe11  26156  fta1lem  26213  vieta1lem2  26217  ispth  29670  dfpth2  29678  uhgrwkspthlem2  29703  usgr2wlkspthlem1  29706  usgr2wlkspthlem2  29707  pthdlem1  29715  2spthd  29890  3spthd  30124  f1o3d  32577  xppreima2  32602  ofpreima  32616  fcnvgreu  32624  mptiffisupp  32643  fpwrelmapffslem  32684  indf1ofs  32818  gsumhashmul  33023  tocycfv  33060  tocycf  33068  cycpm2tr  33070  cycpmconjvlem  33092  evpmval  33096  altgnsg  33100  ply1dg3rt0irred  33527  irngval  33668  ordtrest2NEW  33906  qqhval  33955  esum2dlem  34075  mbfmcst  34243  omssubadd  34284  sitgfval  34325  eulerpartlemgf  34363  orvcval  34442  pthhashvtx  35121  cvmliftmolem1  35274  cvmliftlem5  35282  cvmliftlem15  35291  cvmlift2lem9a  35296  cvmlift2lem9  35304  ismfs  35542  mthmval  35568  wsuceq123  35808  bj-iminvval2  37188  cnambfre  37668  itg2addnclem2  37672  ftc1anclem1  37693  ftc1anclem6  37698  dfsymrels2  38542  dfsymrel2  38546  cdlemg1finvtrlemN  40574  tendoicbv  40792  tendoi  40793  tendoi2  40794  tendoicl  40795  docaffvalN  41120  docafvalN  41121  dihmeetlem1N  41289  dihglblem5apreN  41290  diophrw  42752  rmxfval  42897  rmyfval  42898  aomclem8  43054  cnvtrclfv  43717  frege131d  43757  dssmapnvod  44013  smfpimioo  46788  smfpimcc  46809  smfsuplem2  46813  upgrimpths  47913  dftpos5  48878  tposideq  48892  invfn  49035  invpropdlem  49043  imaidfu  49115  idfth  49163  idsubc  49165  swapf1a  49274  swapf2a  49276  swapf1  49277  swapf2  49279