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

Theorem cnveqd 4857
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 4855 . 2  |-  ( A  =  B  ->  `' A  =  `' B
)
31, 2syl 15 1  |-  ( ph  ->  `' A  =  `' B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   `'ccnv 4688
This theorem is referenced by:  cnvsng  5158  opswap  5159  cores2  5185  suppssof1  6119  2ndval2  6138  2nd1st  6165  cnvf1olem  6216  fparlem3  6220  fparlem4  6221  brtpos2  6240  dftpos4  6253  tpostpos  6254  tposf12  6259  xpcomco  6952  cantnfval  7369  cantnffval2  7397  cnfcomlem  7402  fseqenlem2  7652  dfac12lem1  7769  dfac12r  7772  fpwwe2cbv  8252  fpwwe2lem2  8254  fpwwe2lem6  8257  fpwwe2lem9  8260  fpwwecbv  8266  fpwwelem  8267  fsumcnv  12236  bitsf1ocnv  12635  vdwpc  13027  imasval  13414  xpsfval  13469  xpsval  13474  monfval  13635  ismon  13636  monpropd  13640  isepi  13643  invffval  13660  invfval  13661  oppcinv  13678  isfth  13788  catcisolem  13938  oduval  14234  oduleval  14235  gsumvalx  14451  grpinvcnv  14536  grplactcnv  14564  eqglact  14668  gsumval3  15191  gsumcom2  15226  isunit  15439  issrng  15615  rrgsupp  16032  psrbagaddcl  16116  mplsubrg  16184  evlslem4  16245  evlslem2  16249  coe1sfi  16293  ply1coe  16368  znval  16489  znle2  16507  ptbasfi  17276  ptval2  17296  ptrescn  17333  xkoptsub  17348  qtopval  17386  txswaphmeolem  17495  xpstopnlem2  17502  ptcmpg  17751  tgplacthmeo  17786  prdsxmslem2  18075  nghmfval  18231  isnghm  18232  pi1xfrcnv  18555  ismbf1  18981  ismbf  18985  mbfconst  18990  mbfres2  19000  cncombf  19013  evlslem6  19397  tdeglem4  19446  mdeg0  19456  mdegvsca  19462  deg1val  19482  deg1mul3  19501  fta1glem2  19552  fta1g  19553  fta1b  19555  plypf1  19594  dgrval  19610  dgrlem  19611  coe11  19634  fta1lem  19687  vieta1lem2  19691  jensen  20283  f1o3d  23037  fimacnvinrn  23199  xppreima2  23212  mbfmcst  23564  indf1ofs  23609  orvcval  23658  cvmliftmolem1  23812  cvmliftlem5  23820  cvmliftlem15  23829  cvmlift2lem9a  23834  cvmlift2lem9  23842  relexpcnv  24029  relexprel  24031  valcurfn1  25204  diophrw  26838  rmxfval  26989  rmyfval  26990  aomclem8  27159  frlmup1  27250  cdlemg1finvtrlemN  30764  tendoicbv  30982  tendoi  30983  tendoi2  30984  tendoicl  30985  docaffvalN  31311  docafvalN  31312  dihmeetlem1N  31480  dihglblem5apreN  31481
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-in 3159  df-ss 3166  df-br 4024  df-opab 4078  df-cnv 4697
  Copyright terms: Public domain W3C validator