Theorem cnveqd 5874

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3955  df-ss 3965  df-br 5149  df-opab 5211  df-cnv 5684

This theorem is referenced by:  opswap  6226  cores2  6256  fimacnvinrn  7071  nvocnv  7276  2ndval2  7990  2nd1st  8021  cnvf1olem  8093  fparlem3  8097  fparlem4  8098  brtpos2  8214  dftpos4  8227  tpostpos  8228  tposf12  8233  xpcomco  9059  infeq123d  9473  cantnffval2  9687  cnfcomlem  9691  fseqenlem2  10017  dfac12lem1  10135  dfac12r  10138  fpwwe2cbv  10622  fpwwe2lem2  10624  fpwwe2lem5  10627  fpwwe2lem8  10630  fpwwecbv  10636  fpwwelem  10637  funcnvs2  14861  funcnvs3  14862  funcnvs4  14863  relexpcnv  14979  fsumcnv  15716  fprodcnv  15924  bitsf1ocnv  16382  vdwpc  16910  imasval  17454  xpsval  17513  monfval  17676  ismon  17677  monpropd  17681  isepi  17684  invffval  17702  invfval  17703  dfiso2  17716  isofn  17719  oppcinv  17724  isfth  17862  catcisolem  18057  oduval  18238  oduleval  18239  gsumvalx  18592  grpinvcnv  18888  grplactcnv  18923  eqglact  19054  gsumcom2  19838  isunit  20180  issrng  20451  znval  21079  znle2  21101  evpmss  21131  psgnevpmb  21132  ptbasfi  23077  ptval2  23097  ptrescn  23135  xkoptsub  23150  qtopval  23191  txswaphmeolem  23300  ptcmpg  23553  tgplacthmeo  23599  trust  23726  prdsxmslem2  24030  metuval  24050  nghmfval  24231  isnghm  24232  pi1xfrcnv  24565  ismbf1  25133  ismbf  25137  mbfconst  25142  mbfres2  25154  cncombf  25167  deg1val  25606  fta1glem2  25676  fta1g  25677  fta1b  25679  dgrval  25734  dgrlem  25735  coe11  25759  fta1lem  25812  vieta1lem2  25816  ispth  28970  uhgrwkspthlem2  29001  usgr2wlkspthlem1  29004  usgr2wlkspthlem2  29005  pthdlem1  29013  2spthd  29185  3spthd  29419  f1o3d  31839  xppreima2  31864  ofpreima  31878  fcnvgreu  31886  mptiffisupp  31903  fpwrelmapffslem  31945  gsumhashmul  32196  tocycfv  32256  tocycf  32264  cycpm2tr  32266  cycpmconjvlem  32288  evpmval  32292  altgnsg  32296  irngval  32738  ordtrest2NEW  32892  qqhval  32943  indf1ofs  33013  esum2dlem  33079  mbfmcst  33247  omssubadd  33288  sitgfval  33329  eulerpartlemgf  33367  orvcval  33445  pthhashvtx  34107  cvmliftmolem1  34261  cvmliftlem5  34269  cvmliftlem15  34278  cvmlift2lem9a  34283  cvmlift2lem9  34291  ismfs  34529  mthmval  34555  wsuceq123  34775  bj-iminvval2  36064  cnambfre  36525  itg2addnclem2  36529  ftc1anclem1  36550  ftc1anclem6  36555  dfsymrels2  37404  dfsymrel2  37408  cdlemg1finvtrlemN  39435  tendoicbv  39653  tendoi  39654  tendoi2  39655  tendoicl  39656  docaffvalN  39981  docafvalN  39982  dihmeetlem1N  40150  dihglblem5apreN  40151  diophrw  41483  rmxfval  41628  rmyfval  41629  aomclem8  41789  cnvtrclfv  42461  frege131d  42501  dssmapnvod  42757  smfpimioo  45490  smfpimcc  45511  smfsuplem2  45515