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

Theorem cnveqd 4894
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 4892 . 2  |-  ( A  =  B  ->  `' A  =  `' B
)
31, 2syl 15 1  |-  ( ph  ->  `' A  =  `' B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1633   `'ccnv 4725
This theorem is referenced by:  cnvsng  5195  opswap  5196  cores2  5222  suppssof1  6161  2ndval2  6180  2nd1st  6207  cnvf1olem  6258  fparlem3  6262  fparlem4  6263  brtpos2  6282  dftpos4  6295  tpostpos  6296  tposf12  6301  xpcomco  6995  cantnfval  7414  cantnffval2  7442  cnfcomlem  7447  fseqenlem2  7697  dfac12lem1  7814  dfac12r  7817  fpwwe2cbv  8297  fpwwe2lem2  8299  fpwwe2lem6  8302  fpwwe2lem9  8305  fpwwecbv  8311  fpwwelem  8312  fsumcnv  12283  bitsf1ocnv  12682  vdwpc  13074  imasval  13463  xpsfval  13518  xpsval  13523  monfval  13684  ismon  13685  monpropd  13689  isepi  13692  invffval  13709  invfval  13710  oppcinv  13727  isfth  13837  catcisolem  13987  oduval  14283  oduleval  14284  gsumvalx  14500  grpinvcnv  14585  grplactcnv  14613  eqglact  14717  gsumval3  15240  gsumcom2  15275  isunit  15488  issrng  15664  rrgsupp  16081  psrbagaddcl  16165  mplsubrg  16233  evlslem4  16294  evlslem2  16298  coe1sfi  16342  ply1coe  16417  znval  16545  znle2  16563  ptbasfi  17332  ptval2  17352  ptrescn  17389  xkoptsub  17404  qtopval  17442  txswaphmeolem  17551  xpstopnlem2  17558  ptcmpg  17803  tgplacthmeo  17838  prdsxmslem2  18127  nghmfval  18283  isnghm  18284  pi1xfrcnv  18608  ismbf1  19034  ismbf  19038  mbfconst  19043  mbfres2  19053  cncombf  19066  evlslem6  19450  tdeglem4  19499  mdeg0  19509  mdegvsca  19515  deg1val  19535  deg1mul3  19554  fta1glem2  19605  fta1g  19606  fta1b  19608  plypf1  19647  dgrval  19663  dgrlem  19664  coe11  19687  fta1lem  19740  vieta1lem2  19744  jensen  20336  f1o3d  23191  fimacnvinrn  23197  xppreima2  23209  trust  23441  metuval  23491  qqhval  23553  mbfmcst  23783  indf1ofs  23838  orvcval  23889  cvmliftmolem1  24096  cvmliftlem5  24104  cvmliftlem15  24113  cvmlift2lem9a  24118  cvmlift2lem9  24126  relexpcnv  24313  relexprel  24315  itg2addnclem2  25318  diophrw  25986  rmxfval  26137  rmyfval  26138  aomclem8  26307  frlmup1  26398  ispth  27470  1pthonlem1  27485  2pthonlem1  27495  constr3pthlem2  27540  cdlemg1finvtrlemN  30582  tendoicbv  30800  tendoi  30801  tendoi2  30802  tendoicl  30803  docaffvalN  31129  docafvalN  31130  dihmeetlem1N  31298  dihglblem5apreN  31299
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-in 3193  df-ss 3200  df-br 4061  df-opab 4115  df-cnv 4734
  Copyright terms: Public domain W3C validator