Theorem cnveqd 5712

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3399  df-in 3848  df-ss 3858  df-br 5028  df-opab 5090  df-cnv 5527

This theorem is referenced by:  opswap  6055  cores2  6086  fimacnvinrn  6843  nvocnv  7043  2ndval2  7725  2nd1st  7755  cnvf1olem  7824  fparlem3  7828  fparlem4  7829  brtpos2  7920  dftpos4  7933  tpostpos  7934  tposf12  7939  xpcomco  8649  infeq123d  9011  cantnffval2  9224  cnfcomlem  9228  fseqenlem2  9518  dfac12lem1  9636  dfac12r  9639  fpwwe2cbv  10123  fpwwe2lem2  10125  fpwwe2lem5  10128  fpwwe2lem8  10131  fpwwecbv  10137  fpwwelem  10138  funcnvs2  14357  funcnvs3  14358  funcnvs4  14359  relexpcnv  14477  fsumcnv  15214  fprodcnv  15422  bitsf1ocnv  15880  vdwpc  16409  imasval  16880  xpsval  16939  monfval  17100  ismon  17101  monpropd  17105  isepi  17108  invffval  17126  invfval  17127  dfiso2  17140  isofn  17143  oppcinv  17148  isfth  17282  catcisolem  17475  oduval  17849  oduleval  17850  gsumvalx  17995  grpinvcnv  18278  grplactcnv  18313  eqglact  18442  gsumcom2  19207  isunit  19522  issrng  19733  znval  20347  znle2  20365  evpmss  20395  psgnevpmb  20396  ptbasfi  22325  ptval2  22345  ptrescn  22383  xkoptsub  22398  qtopval  22439  txswaphmeolem  22548  ptcmpg  22801  tgplacthmeo  22847  trust  22974  prdsxmslem2  23275  metuval  23295  nghmfval  23468  isnghm  23469  pi1xfrcnv  23802  ismbf1  24369  ismbf  24373  mbfconst  24378  mbfres2  24390  cncombf  24403  deg1val  24841  fta1glem2  24911  fta1g  24912  fta1b  24914  dgrval  24969  dgrlem  24970  coe11  24994  fta1lem  25047  vieta1lem2  25051  ispth  27656  uhgrwkspthlem2  27687  usgr2wlkspthlem1  27690  usgr2wlkspthlem2  27691  pthdlem1  27699  2spthd  27871  3spthd  28105  f1o3d  30528  xppreima2  30554  ofpreima  30569  fcnvgreu  30577  fpwrelmapffslem  30634  gsumhashmul  30885  tocycfv  30945  tocycf  30953  cycpm2tr  30955  cycpmconjvlem  30977  evpmval  30981  altgnsg  30985  ordtrest2NEW  31437  qqhval  31486  indf1ofs  31556  esum2dlem  31622  mbfmcst  31788  omssubadd  31829  sitgfval  31870  eulerpartlemgf  31908  orvcval  31986  pthhashvtx  32652  cvmliftmolem1  32806  cvmliftlem5  32814  cvmliftlem15  32823  cvmlift2lem9a  32828  cvmlift2lem9  32836  ismfs  33074  mthmval  33100  wsuceq123  33411  bj-iminvval2  34975  cnambfre  35437  itg2addnclem2  35441  ftc1anclem1  35462  ftc1anclem6  35467  dfsymrels2  36271  dfsymrel2  36275  cdlemg1finvtrlemN  38201  tendoicbv  38419  tendoi  38420  tendoi2  38421  tendoicl  38422  docaffvalN  38747  docafvalN  38748  dihmeetlem1N  38916  dihglblem5apreN  38917  diophrw  40137  rmxfval  40282  rmyfval  40283  aomclem8  40442  cnvtrclfv  40862  frege131d  40902  dssmapnvod  41158  smfpimioo  43844  smfpimcc  43864  smfsuplem2  43868