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

Theorem cnveqd 5041
Description: Equality deduction for converse. (Contributed by NM, 6-Dec-2013.)
Hypothesis
Ref Expression
cnveqd.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
cnveqd  |-  ( ph  ->  `' A  =  `' B )

Proof of Theorem cnveqd
StepHypRef Expression
1 cnveqd.1 . 2  |-  ( ph  ->  A  =  B )
2 cnveq 5039 . 2  |-  ( A  =  B  ->  `' A  =  `' B
)
31, 2syl 16 1  |-  ( ph  ->  `' A  =  `' B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   `'ccnv 4870
This theorem is referenced by:  cnvsng  5348  opswap  5349  cores2  5375  suppssof1  6339  2ndval2  6358  2nd1st  6385  cnvf1olem  6437  fparlem3  6441  fparlem4  6442  brtpos2  6478  dftpos4  6491  tpostpos  6492  tposf12  6497  xpcomco  7191  cantnfval  7616  cantnffval2  7644  cnfcomlem  7649  fseqenlem2  7899  dfac12lem1  8016  dfac12r  8019  fpwwe2cbv  8498  fpwwe2lem2  8500  fpwwe2lem6  8503  fpwwe2lem9  8506  fpwwecbv  8512  fpwwelem  8513  fsumcnv  12550  bitsf1ocnv  12949  vdwpc  13341  imasval  13730  xpsfval  13785  xpsval  13790  monfval  13951  ismon  13952  monpropd  13956  isepi  13959  invffval  13976  invfval  13977  oppcinv  13994  isfth  14104  catcisolem  14254  oduval  14550  oduleval  14551  gsumvalx  14767  grpinvcnv  14852  grplactcnv  14880  eqglact  14984  gsumval3  15507  gsumcom2  15542  isunit  15755  issrng  15931  rrgsupp  16344  psrbagaddcl  16428  mplsubrg  16496  evlslem4  16557  evlslem2  16561  coe1sfi  16603  ply1coe  16677  znval  16809  znle2  16827  ptbasfi  17606  ptval2  17626  ptrescn  17664  xkoptsub  17679  qtopval  17720  txswaphmeolem  17829  xpstopnlem2  17836  ptcmpg  18081  tgplacthmeo  18126  trust  18252  prdsxmslem2  18552  metuvalOLD  18572  metuval  18573  nghmfval  18749  isnghm  18750  pi1xfrcnv  19075  ismbf1  19511  ismbf  19515  mbfconst  19520  mbfres2  19530  cncombf  19543  evlslem6  19927  tdeglem4  19976  mdeg0  19986  mdegvsca  19992  deg1val  20012  deg1mul3  20031  fta1glem2  20082  fta1g  20083  fta1b  20085  plypf1  20124  dgrval  20140  dgrlem  20141  coe11  20164  fta1lem  20217  vieta1lem2  20221  jensen  20820  ispth  21561  1pthonlem1  21582  constr2spthlem1  21587  2pthlem1  21588  constr2pth  21594  constr3pthlem2  21636  f1o3d  24034  fimacnvinrn  24040  xppreima2  24053  ofpreima  24074  qqhval  24351  indf1ofs  24416  mbfmcst  24602  sitgfval  24648  orvcval  24708  cvmliftmolem1  24961  cvmliftlem5  24969  cvmliftlem15  24978  cvmlift2lem9a  24983  cvmlift2lem9  24991  relexpcnv  25126  relexprel  25127  fprodcnv  25300  wsuceq123  25558  cnambfre  26246  itg2addnclem2  26248  ftc1anclem1  26271  ftc1anclem6  26276  diophrw  26809  rmxfval  26959  rmyfval  26960  aomclem8  27128  frlmup1  27219  usgra2pthspth  28259  cdlemg1finvtrlemN  31310  tendoicbv  31528  tendoi  31529  tendoi2  31530  tendoicl  31531  docaffvalN  31857  docafvalN  31858  dihmeetlem1N  32026  dihglblem5apreN  32027
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-in 3320  df-ss 3327  df-br 4206  df-opab 4260  df-cnv 4879
  Copyright terms: Public domain W3C validator