Theorem cnveqd 5849

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ^◡ccnv 5646

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3915  df-br 5103  df-opab 5167  df-cnv 5655

This theorem is used by:  csbcnv  5860  opswap  6219  cores2  6250  fimacnvinrn  7059  nvocnv  7277  2ndval2  8002  2nd1st  8032  cnvf1olem  8104  fparlem3  8108  fparlem4  8109  brtpos2  8227  dftpos4  8240  tpostpos  8241  tposf12  8246  xpcomco  9064  infeq123d  9452  cantnffval2  9674  cnfcomlem  9678  fseqenlem2  10075  dfac12lem1  10193  dfac12r  10196  fpwwe2cbv  10686  fpwwe2lem2  10688  fpwwe2lem5  10691  fpwwe2lem8  10694  fpwwecbv  10700  fpwwelem  10701  funcnvs2  15031  funcnvs3  15032  funcnvs4  15033  relexpcnv  15155  fsumcnv  15906  fprodcnv  16117  bitsf1ocnv  16581  vdwpc  17119  imasval  17644  xpsval  17703  monfval  17868  ismon  17869  monpropd  17873  isepi  17876  invffval  17894  invfval  17895  dfiso2  17908  isofn  17911  oppcinv  17916  isfth  18052  catcisolem  18246  oduval  18423  oduleval  18424  gsumvalx  18826  grpinvcnv  19178  grplactcnv  19214  eqglact  19352  gsumcom2  20150  isunit  20564  issrng  21062  znval  21802  znle2  21820  evpmss  21853  psgnevpmb  21854  ptbasfi  23861  ptval2  23881  ptrescn  23919  xkoptsub  23934  qtopval  23975  txswaphmeolem  24084  ptcmpg  24337  tgplacthmeo  24383  trust  24509  prdsxmslem2  24809  metuval  24829  nghmfval  25002  isnghm  25003  pi1xfrcnv  25339  ismbf1  25906  ismbf  25910  mbfconst  25915  mbfres2  25927  cncombf  25940  deg1val  26375  fta1glem2  26448  fta1g  26449  fta1b  26451  dgrval  26508  dgrlem  26509  coe11  26533  fta1lem  26591  vieta1lem2  26597  ispth  30239  dfpth2  30247  pthhashvtx  30248  uhgrwkspthlem2  30273  usgr2wlkspthlem1  30276  usgr2wlkspthlem2  30277  pthdlem1  30285  2spthd  30463  3spthd  30710  f1o3d  33153  xppreima2  33178  ofpreima  33192  fcnvgreu  33199  mptiffisupp  33219  fpwrelmapffslem  33257  indf1ofs  33366  gsumhashmul  33561  tocycfv  33603  tocycf  33611  cycpm2tr  33613  cycpmconjvlem  33635  evpmval  33639  altgnsg  33643  ply1dg3rt0irred  34049  vieta  34145  irngval  34250  ordtrest2NEW  34488  qqhval  34537  esum2dlem  34657  mbfmcst  34825  omssubadd  34866  sitgfval  34907  eulerpartlemgf  34945  orvcval  35024  cvmliftmolem1  35967  cvmliftlem5  35975  cvmliftlem15  35984  cvmlift2lem9a  35989  cvmlift2lem9  35997  ismfs  36235  mthmval  36261  wsuceq123  36498  bj-iminvval2  38035  cnambfre  38506  itg2addnclem2  38510  ftc1anclem1  38531  ftc1anclem6  38536  dfsymrels2  39477  dfsymrel2  39485  cdlemg1finvtrlemN  41552  tendoicbv  41770  tendoi  41771  tendoi2  41772  tendoicl  41773  docaffvalN  42098  docafvalN  42099  dihmeetlem1N  42267  dihglblem5apreN  42268  diophrw  43708  rmxfval  43849  rmyfval  43850  aomclem8  44006  cnvtrclfv  44668  frege131d  44708  dssmapnvod  44964  smfpimioo  47719  smfpimcc  47740  smfsuplem2  47744  upgrimpths  48929  dftpos5  49904  tposideq  49918  invfn  50060  invpropdlem  50068  imaidfu  50140  idfth  50188  idsubc  50190  swapf1a  50299  swapf2a  50301  swapf1  50302  swapf2  50304