Theorem cnveqd 5748

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

Syntax hints:   → wi 4   = wceq 1537  ^◡ccnv 5556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-in 3945  df-ss 3954  df-br 5069  df-opab 5131  df-cnv 5565

This theorem is referenced by:  opswap  6088  cores2  6114  fimacnvinrn  6842  nvocnv  7040  2ndval2  7709  2nd1st  7739  cnvf1olem  7807  fparlem3  7811  fparlem4  7812  brtpos2  7900  dftpos4  7913  tpostpos  7914  tposf12  7919  xpcomco  8609  infeq123d  8947  cantnffval2  9160  cnfcomlem  9164  fseqenlem2  9453  dfac12lem1  9571  dfac12r  9574  fpwwe2cbv  10054  fpwwe2lem2  10056  fpwwe2lem6  10059  fpwwe2lem9  10062  fpwwecbv  10068  fpwwelem  10069  funcnvs2  14277  funcnvs3  14278  funcnvs4  14279  relexpcnv  14396  fsumcnv  15130  fprodcnv  15339  bitsf1ocnv  15795  vdwpc  16318  imasval  16786  xpsval  16845  monfval  17004  ismon  17005  monpropd  17009  isepi  17012  invffval  17030  invfval  17031  dfiso2  17044  isofn  17047  oppcinv  17052  isfth  17186  catcisolem  17368  oduval  17742  oduleval  17743  gsumvalx  17888  grpinvcnv  18169  grplactcnv  18204  eqglact  18333  gsumcom2  19097  isunit  19409  issrng  19623  znval  20684  znle2  20702  evpmss  20732  psgnevpmb  20733  ptbasfi  22191  ptval2  22211  ptrescn  22249  xkoptsub  22264  qtopval  22305  txswaphmeolem  22414  ptcmpg  22667  tgplacthmeo  22713  trust  22840  prdsxmslem2  23141  metuval  23161  nghmfval  23333  isnghm  23334  pi1xfrcnv  23663  ismbf1  24227  ismbf  24231  mbfconst  24236  mbfres2  24248  cncombf  24261  deg1val  24692  fta1glem2  24762  fta1g  24763  fta1b  24765  dgrval  24820  dgrlem  24821  coe11  24845  fta1lem  24898  vieta1lem2  24902  ispth  27506  uhgrwkspthlem2  27537  usgr2wlkspthlem1  27540  usgr2wlkspthlem2  27541  pthdlem1  27549  2spthd  27722  3spthd  27957  f1o3d  30374  xppreima2  30397  ofpreima  30412  fcnvgreu  30420  fpwrelmapffslem  30470  tocycfv  30753  tocycf  30761  cycpm2tr  30763  cycpmconjvlem  30785  evpmval  30789  altgnsg  30793  ordtrest2NEW  31168  qqhval  31217  indf1ofs  31287  esum2dlem  31353  mbfmcst  31519  omssubadd  31560  sitgfval  31601  eulerpartlemgf  31639  orvcval  31717  pthhashvtx  32376  cvmliftmolem1  32530  cvmliftlem5  32538  cvmliftlem15  32547  cvmlift2lem9a  32552  cvmlift2lem9  32560  ismfs  32798  mthmval  32824  wsuceq123  33103  cnambfre  34942  itg2addnclem2  34946  ftc1anclem1  34969  ftc1anclem6  34974  dfsymrels2  35783  dfsymrel2  35787  cdlemg1finvtrlemN  37713  tendoicbv  37931  tendoi  37932  tendoi2  37933  tendoicl  37934  docaffvalN  38259  docafvalN  38260  dihmeetlem1N  38428  dihglblem5apreN  38429  diophrw  39363  rmxfval  39508  rmyfval  39509  aomclem8  39668  cnvtrclfv  40076  frege131d  40116  dssmapnvod  40373  smfpimioo  43069  smfpimcc  43089  smfsuplem2  43093