Theorem cnveqd 5886

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

Syntax hints:   → wi 4   = wceq 1540  ^◡ccnv 5684

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ss 3968  df-br 5144  df-opab 5206  df-cnv 5693

This theorem is referenced by:  opswap  6249  cores2  6279  fimacnvinrn  7091  nvocnv  7301  2ndval2  8032  2nd1st  8063  cnvf1olem  8135  fparlem3  8139  fparlem4  8140  brtpos2  8257  dftpos4  8270  tpostpos  8271  tposf12  8276  xpcomco  9102  infeq123d  9521  cantnffval2  9735  cnfcomlem  9739  fseqenlem2  10065  dfac12lem1  10184  dfac12r  10187  fpwwe2cbv  10670  fpwwe2lem2  10672  fpwwe2lem5  10675  fpwwe2lem8  10678  fpwwecbv  10684  fpwwelem  10685  funcnvs2  14952  funcnvs3  14953  funcnvs4  14954  relexpcnv  15074  fsumcnv  15809  fprodcnv  16019  bitsf1ocnv  16481  vdwpc  17018  imasval  17556  xpsval  17615  monfval  17776  ismon  17777  monpropd  17781  isepi  17784  invffval  17802  invfval  17803  dfiso2  17816  isofn  17819  oppcinv  17824  isfth  17961  catcisolem  18155  oduval  18333  oduleval  18334  gsumvalx  18689  grpinvcnv  19024  grplactcnv  19061  eqglact  19197  gsumcom2  19993  isunit  20373  issrng  20845  znval  21550  znle2  21572  evpmss  21604  psgnevpmb  21605  ptbasfi  23589  ptval2  23609  ptrescn  23647  xkoptsub  23662  qtopval  23703  txswaphmeolem  23812  ptcmpg  24065  tgplacthmeo  24111  trust  24238  prdsxmslem2  24542  metuval  24562  nghmfval  24743  isnghm  24744  pi1xfrcnv  25090  ismbf1  25659  ismbf  25663  mbfconst  25668  mbfres2  25680  cncombf  25693  deg1val  26135  fta1glem2  26208  fta1g  26209  fta1b  26211  dgrval  26267  dgrlem  26268  coe11  26292  fta1lem  26349  vieta1lem2  26353  ispth  29741  dfpth2  29749  uhgrwkspthlem2  29774  usgr2wlkspthlem1  29777  usgr2wlkspthlem2  29778  pthdlem1  29786  2spthd  29961  3spthd  30195  f1o3d  32637  xppreima2  32661  ofpreima  32675  fcnvgreu  32683  mptiffisupp  32702  fpwrelmapffslem  32743  indf1ofs  32851  gsumhashmul  33064  tocycfv  33129  tocycf  33137  cycpm2tr  33139  cycpmconjvlem  33161  evpmval  33165  altgnsg  33169  ply1dg3rt0irred  33607  irngval  33735  ordtrest2NEW  33922  qqhval  33973  esum2dlem  34093  mbfmcst  34261  omssubadd  34302  sitgfval  34343  eulerpartlemgf  34381  orvcval  34460  pthhashvtx  35133  cvmliftmolem1  35286  cvmliftlem5  35294  cvmliftlem15  35303  cvmlift2lem9a  35308  cvmlift2lem9  35316  ismfs  35554  mthmval  35580  wsuceq123  35815  bj-iminvval2  37195  cnambfre  37675  itg2addnclem2  37679  ftc1anclem1  37700  ftc1anclem6  37705  dfsymrels2  38546  dfsymrel2  38550  cdlemg1finvtrlemN  40577  tendoicbv  40795  tendoi  40796  tendoi2  40797  tendoicl  40798  docaffvalN  41123  docafvalN  41124  dihmeetlem1N  41292  dihglblem5apreN  41293  diophrw  42770  rmxfval  42915  rmyfval  42916  aomclem8  43073  cnvtrclfv  43737  frege131d  43777  dssmapnvod  44033  smfpimioo  46802  smfpimcc  46823  smfsuplem2  46827  dftpos5  48774  tposideq  48788  swapf1a  48975  swapf2a  48977  swapf1  48978  swapf2  48980