Theorem cnveqd 5852

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

Syntax hints:   → wi 4   = wceq 1539  ^◡ccnv 5650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ss 3941  df-br 5117  df-opab 5179  df-cnv 5659

This theorem is referenced by:  opswap  6215  cores2  6245  fimacnvinrn  7057  nvocnv  7269  2ndval2  8000  2nd1st  8031  cnvf1olem  8103  fparlem3  8107  fparlem4  8108  brtpos2  8225  dftpos4  8238  tpostpos  8239  tposf12  8244  xpcomco  9070  infeq123d  9487  cantnffval2  9701  cnfcomlem  9705  fseqenlem2  10031  dfac12lem1  10150  dfac12r  10153  fpwwe2cbv  10636  fpwwe2lem2  10638  fpwwe2lem5  10641  fpwwe2lem8  10644  fpwwecbv  10650  fpwwelem  10651  funcnvs2  14919  funcnvs3  14920  funcnvs4  14921  relexpcnv  15041  fsumcnv  15776  fprodcnv  15986  bitsf1ocnv  16448  vdwpc  16985  imasval  17510  xpsval  17569  monfval  17730  ismon  17731  monpropd  17735  isepi  17738  invffval  17756  invfval  17757  dfiso2  17770  isofn  17773  oppcinv  17778  isfth  17914  catcisolem  18108  oduval  18285  oduleval  18286  gsumvalx  18639  grpinvcnv  18974  grplactcnv  19011  eqglact  19147  gsumcom2  19941  isunit  20318  issrng  20789  znval  21481  znle2  21499  evpmss  21531  psgnevpmb  21532  ptbasfi  23504  ptval2  23524  ptrescn  23562  xkoptsub  23577  qtopval  23618  txswaphmeolem  23727  ptcmpg  23980  tgplacthmeo  24026  trust  24153  prdsxmslem2  24453  metuval  24473  nghmfval  24646  isnghm  24647  pi1xfrcnv  24993  ismbf1  25562  ismbf  25566  mbfconst  25571  mbfres2  25583  cncombf  25596  deg1val  26038  fta1glem2  26111  fta1g  26112  fta1b  26114  dgrval  26170  dgrlem  26171  coe11  26195  fta1lem  26252  vieta1lem2  26256  ispth  29635  dfpth2  29643  uhgrwkspthlem2  29668  usgr2wlkspthlem1  29671  usgr2wlkspthlem2  29672  pthdlem1  29680  2spthd  29855  3spthd  30089  f1o3d  32538  xppreima2  32562  ofpreima  32576  fcnvgreu  32584  mptiffisupp  32603  fpwrelmapffslem  32644  indf1ofs  32761  gsumhashmul  32973  tocycfv  33038  tocycf  33046  cycpm2tr  33048  cycpmconjvlem  33070  evpmval  33074  altgnsg  33078  ply1dg3rt0irred  33512  irngval  33642  ordtrest2NEW  33862  qqhval  33911  esum2dlem  34031  mbfmcst  34199  omssubadd  34240  sitgfval  34281  eulerpartlemgf  34319  orvcval  34398  pthhashvtx  35071  cvmliftmolem1  35224  cvmliftlem5  35232  cvmliftlem15  35241  cvmlift2lem9a  35246  cvmlift2lem9  35254  ismfs  35492  mthmval  35518  wsuceq123  35753  bj-iminvval2  37133  cnambfre  37613  itg2addnclem2  37617  ftc1anclem1  37638  ftc1anclem6  37643  dfsymrels2  38484  dfsymrel2  38488  cdlemg1finvtrlemN  40515  tendoicbv  40733  tendoi  40734  tendoi2  40735  tendoicl  40736  docaffvalN  41061  docafvalN  41062  dihmeetlem1N  41230  dihglblem5apreN  41231  diophrw  42707  rmxfval  42852  rmyfval  42853  aomclem8  43010  cnvtrclfv  43673  frege131d  43713  dssmapnvod  43969  smfpimioo  46746  smfpimcc  46767  smfsuplem2  46771  dftpos5  48729  tposideq  48743  invfn  48879  invpropdlem  48884  swapf1a  48992  swapf2a  48994  swapf1  48995  swapf2  48997