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 18	1 ⊢ (𝜑 → ◡𝐴 = ◡𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ^◡ccnv 5649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3896  df-br 5103  df-opab 5167  df-cnv 5658

This theorem is used by:  csbcnv  5863  opswap  6230  cores2  6261  fimacnvinrn  7071  nvocnv  7289  2ndval2  8019  2nd1st  8049  cnvf1olem  8121  fparlem3  8125  fparlem4  8126  brtpos2  8249  dftpos4  8262  tpostpos  8263  tposf12  8268  xpcomco  9086  infeq123d  9474  cantnffval2  9696  cnfcomlem  9700  fseqenlem2  10104  dfac12lem1  10222  dfac12r  10225  fpwwe2cbv  10715  fpwwe2lem2  10717  fpwwe2lem5  10720  fpwwe2lem8  10723  fpwwecbv  10729  fpwwelem  10730  funcnvs2  15064  funcnvs3  15065  funcnvs4  15066  relexpcnv  15188  fsumcnv  15939  fprodcnv  16150  bitsf1ocnv  16614  vdwpc  17158  imasval  17683  xpsval  17742  monfval  17907  ismon  17908  monpropd  17912  isepi  17915  invffval  17933  invfval  17934  dfiso2  17947  isofn  17950  oppcinv  17955  isfth  18091  catcisolem  18285  oduval  18462  oduleval  18463  gsumvalx  18865  grpinvcnv  19217  grplactcnv  19253  eqglact  19391  gsumcom2  20189  isunit  20603  issrng  21101  znval  21841  znle2  21859  evpmss  21892  psgnevpmb  21893  ptbasfi  23900  ptval2  23920  ptrescn  23958  xkoptsub  23973  qtopval  24014  txswaphmeolem  24123  ptcmpg  24376  tgplacthmeo  24422  trust  24548  prdsxmslem2  24848  metuval  24868  nghmfval  25041  isnghm  25042  pi1xfrcnv  25378  ismbf1  25945  ismbf  25949  mbfconst  25954  mbfres2  25966  cncombf  25979  deg1val  26414  fta1glem2  26487  fta1g  26488  fta1b  26490  dgrval  26547  dgrlem  26548  coe11  26572  fta1lem  26628  vieta1lem2  26634  ispth  30306  dfpth2  30314  pthhashvtx  30315  uhgrwkspthlem2  30340  usgr2wlkspthlem1  30343  usgr2wlkspthlem2  30344  pthdlem1  30352  2spthd  30530  3spthd  30777  f1o3d  33220  xppreima2  33245  ofpreima  33259  fcnvgreu  33266  mptiffisupp  33286  fpwrelmapffslem  33324  indf1ofs  33433  gsumhashmul  33628  tocycfv  33670  tocycf  33678  cycpm2tr  33680  cycpmconjvlem  33702  evpmval  33706  altgnsg  33710  ply1dg3rt0irred  34116  vieta  34212  irngval  34317  ordtrest2NEW  34555  qqhval  34604  esum2dlem  34724  mbfmcst  34891  omssubadd  34932  sitgfval  34973  eulerpartlemgf  35011  orvcval  35090  cvmliftmolem1  36046  cvmliftlem5  36054  cvmliftlem15  36063  cvmlift2lem9a  36068  cvmlift2lem9  36076  ismfs  36314  mthmval  36340  wsuceq123  36576  bj-iminvval2  38116  cnambfre  38587  itg2addnclem2  38591  ftc1anclem1  38612  ftc1anclem6  38617  dfsymrels2  39558  dfsymrel2  39566  cdlemg1finvtrlemN  41633  tendoicbv  41851  tendoi  41852  tendoi2  41853  tendoicl  41854  docaffvalN  42179  docafvalN  42180  dihmeetlem1N  42348  dihglblem5apreN  42349  diophrw  43770  rmxfval  43911  rmyfval  43912  aomclem8  44063  cnvtrclfv  44724  frege131d  44764  dssmapnvod  45020  smfpimioo  47797  smfpimcc  47818  smfsuplem2  47822  upgrimpths  49007  dftpos5  49982  tposideq  49996  invfn  50138  invpropdlem  50146  imaidfu  50218  idfth  50266  idsubc  50268  swapf1a  50377  swapf2a  50379  swapf1  50380  swapf2  50382