Theorem cnveqd 5820

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

Syntax hints:   → wi 4   = wceq 1548  ^◡ccnv 5620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ss 3902  df-br 5076  df-opab 5138  df-cnv 5629

This theorem is referenced by:  csbcnv  5831  opswap  6184  cores2  6215  fimacnvinrn  7016  nvocnv  7229  2ndval2  7953  2nd1st  7984  cnvf1olem  8053  fparlem3  8057  fparlem4  8058  brtpos2  8176  dftpos4  8189  tpostpos  8190  tposf12  8195  xpcomco  8999  infeq123d  9389  cantnffval2  9611  cnfcomlem  9615  fseqenlem2  9942  dfac12lem1  10061  dfac12r  10064  fpwwe2cbv  10548  fpwwe2lem2  10550  fpwwe2lem5  10553  fpwwe2lem8  10556  fpwwecbv  10562  fpwwelem  10563  funcnvs2  14870  funcnvs3  14871  funcnvs4  14872  relexpcnv  14992  fsumcnv  15730  fprodcnv  15943  bitsf1ocnv  16408  vdwpc  16946  imasval  17470  xpsval  17529  monfval  17694  ismon  17695  monpropd  17699  isepi  17702  invffval  17720  invfval  17721  dfiso2  17734  isofn  17737  oppcinv  17742  isfth  17878  catcisolem  18072  oduval  18249  oduleval  18250  gsumvalx  18639  grpinvcnv  18977  grplactcnv  19014  eqglact  19149  gsumcom2  19945  isunit  20348  issrng  20820  znval  21514  znle2  21532  evpmss  21565  psgnevpmb  21566  ptbasfi  23568  ptval2  23588  ptrescn  23626  xkoptsub  23641  qtopval  23682  txswaphmeolem  23791  ptcmpg  24044  tgplacthmeo  24090  trust  24216  prdsxmslem2  24516  metuval  24536  nghmfval  24709  isnghm  24710  pi1xfrcnv  25046  ismbf1  25613  ismbf  25617  mbfconst  25622  mbfres2  25634  cncombf  25647  deg1val  26083  fta1glem2  26156  fta1g  26157  fta1b  26159  dgrval  26215  dgrlem  26216  coe11  26240  fta1lem  26295  vieta1lem2  26299  ispth  29811  dfpth2  29819  uhgrwkspthlem2  29844  usgr2wlkspthlem1  29847  usgr2wlkspthlem2  29848  pthdlem1  29856  2spthd  30031  3spthd  30268  f1o3d  32722  xppreima2  32747  ofpreima  32761  fcnvgreu  32768  mptiffisupp  32789  fpwrelmapffslem  32828  indf1ofs  32949  gsumhashmul  33152  tocycfv  33194  tocycf  33202  cycpm2tr  33204  cycpmconjvlem  33226  evpmval  33230  altgnsg  33234  ply1dg3rt0irred  33679  vieta  33776  irngval  33881  ordtrest2NEW  34119  qqhval  34168  esum2dlem  34288  mbfmcst  34455  omssubadd  34496  sitgfval  34537  eulerpartlemgf  34575  orvcval  34654  pthhashvtx  35371  cvmliftmolem1  35524  cvmliftlem5  35532  cvmliftlem15  35541  cvmlift2lem9a  35546  cvmlift2lem9  35554  ismfs  35792  mthmval  35818  wsuceq123  36055  bj-iminvval2  37569  cnambfre  38050  itg2addnclem2  38054  ftc1anclem1  38075  ftc1anclem6  38080  dfsymrels2  39007  dfsymrel2  39015  cdlemg1finvtrlemN  41082  tendoicbv  41300  tendoi  41301  tendoi2  41302  tendoicl  41303  docaffvalN  41628  docafvalN  41629  dihmeetlem1N  41797  dihglblem5apreN  41798  diophrw  43223  rmxfval  43364  rmyfval  43365  aomclem8  43521  cnvtrclfv  44183  frege131d  44223  dssmapnvod  44479  smfpimioo  47244  smfpimcc  47265  smfsuplem2  47269  upgrimpths  48414  dftpos5  49378  tposideq  49392  invfn  49534  invpropdlem  49542  imaidfu  49614  idfth  49662  idsubc  49664  swapf1a  49773  swapf2a  49775  swapf1  49776  swapf2  49778