MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnveqd Structured version   Visualization version   GIF version

Theorem cnveqd 5739
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
StepHypRef Expression
1 cnveqd.1 . 2 (𝜑𝐴 = 𝐵)
2 cnveq 5737 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
31, 2syl 17 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  ccnv 5547
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-in 3941  df-ss 3950  df-br 5058  df-opab 5120  df-cnv 5556
This theorem is referenced by:  opswap  6079  cores2  6105  fimacnvinrn  6833  nvocnv  7030  2ndval2  7699  2nd1st  7729  cnvf1olem  7797  fparlem3  7801  fparlem4  7802  brtpos2  7890  dftpos4  7903  tpostpos  7904  tposf12  7909  xpcomco  8599  infeq123d  8937  cantnffval2  9150  cnfcomlem  9154  fseqenlem2  9443  dfac12lem1  9561  dfac12r  9564  fpwwe2cbv  10044  fpwwe2lem2  10046  fpwwe2lem6  10049  fpwwe2lem9  10052  fpwwecbv  10058  fpwwelem  10059  funcnvs2  14267  funcnvs3  14268  funcnvs4  14269  relexpcnv  14386  fsumcnv  15120  fprodcnv  15329  bitsf1ocnv  15785  vdwpc  16308  imasval  16776  xpsval  16835  monfval  16994  ismon  16995  monpropd  16999  isepi  17002  invffval  17020  invfval  17021  dfiso2  17034  isofn  17037  oppcinv  17042  isfth  17176  catcisolem  17358  oduval  17732  oduleval  17733  gsumvalx  17878  grpinvcnv  18159  grplactcnv  18194  eqglact  18323  gsumcom2  19087  isunit  19399  issrng  19613  znval  20674  znle2  20692  evpmss  20722  psgnevpmb  20723  ptbasfi  22181  ptval2  22201  ptrescn  22239  xkoptsub  22254  qtopval  22295  txswaphmeolem  22404  ptcmpg  22657  tgplacthmeo  22703  trust  22830  prdsxmslem2  23131  metuval  23151  nghmfval  23323  isnghm  23324  pi1xfrcnv  23653  ismbf1  24217  ismbf  24221  mbfconst  24226  mbfres2  24238  cncombf  24251  deg1val  24682  fta1glem2  24752  fta1g  24753  fta1b  24755  dgrval  24810  dgrlem  24811  coe11  24835  fta1lem  24888  vieta1lem2  24892  ispth  27496  uhgrwkspthlem2  27527  usgr2wlkspthlem1  27530  usgr2wlkspthlem2  27531  pthdlem1  27539  2spthd  27712  3spthd  27947  f1o3d  30364  xppreima2  30387  ofpreima  30402  fcnvgreu  30410  fpwrelmapffslem  30460  tocycfv  30744  tocycf  30752  cycpm2tr  30754  cycpmconjvlem  30776  evpmval  30780  altgnsg  30784  ordtrest2NEW  31154  qqhval  31203  indf1ofs  31273  esum2dlem  31339  mbfmcst  31505  omssubadd  31546  sitgfval  31587  eulerpartlemgf  31625  orvcval  31703  pthhashvtx  32362  cvmliftmolem1  32516  cvmliftlem5  32524  cvmliftlem15  32533  cvmlift2lem9a  32538  cvmlift2lem9  32546  ismfs  32784  mthmval  32810  wsuceq123  33089  cnambfre  34927  itg2addnclem2  34931  ftc1anclem1  34954  ftc1anclem6  34959  dfsymrels2  35768  dfsymrel2  35772  cdlemg1finvtrlemN  37698  tendoicbv  37916  tendoi  37917  tendoi2  37918  tendoicl  37919  docaffvalN  38244  docafvalN  38245  dihmeetlem1N  38413  dihglblem5apreN  38414  diophrw  39341  rmxfval  39486  rmyfval  39487  aomclem8  39646  cnvtrclfv  40054  frege131d  40094  dssmapnvod  40351  smfpimioo  43047  smfpimcc  43067  smfsuplem2  43071
  Copyright terms: Public domain W3C validator