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

Theorem cnveqd 5021
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 5019 . 2  |-  ( A  =  B  ->  `' A  =  `' B
)
31, 2syl 17 1  |-  ( ph  ->  `' A  =  `' B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437   `'ccnv 4844
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-in 3440  df-ss 3447  df-br 4418  df-opab 4476  df-cnv 4853
This theorem is referenced by:  cnvsng  5333  opswap  5334  cores2  5359  nvocnv  6186  2ndval2  6816  2nd1st  6843  cnvf1olem  6896  fparlem3  6900  fparlem4  6901  brtpos2  6978  dftpos4  6991  tpostpos  6992  tposf12  6997  xpcomco  7659  infeq123d  7994  cantnffval2  8190  cnfcomlem  8194  fseqenlem2  8445  dfac12lem1  8562  dfac12r  8565  fpwwe2cbv  9044  fpwwe2lem2  9046  fpwwe2lem6  9049  fpwwe2lem9  9052  fpwwecbv  9058  fpwwelem  9059  relexpcnv  13066  fsumcnv  13801  fprodcnv  14004  bitsf1ocnv  14381  vdwpc  14882  imasval  15361  xpsfval  15417  xpsval  15422  monfval  15581  ismon  15582  monpropd  15586  isepi  15589  invffval  15607  invfval  15608  dfiso2  15621  isofn  15624  oppcinv  15629  isfth  15763  catcisolem  15945  oduval  16320  oduleval  16321  gsumvalx  16457  grpinvcnv  16666  grplactcnv  16698  eqglact  16812  gsumcom2  17535  isunit  17813  issrng  18006  znval  19030  znle2  19048  evpmss  19078  psgnevpmb  19079  ptbasfi  20520  ptval2  20540  ptrescn  20578  xkoptsub  20593  qtopval  20634  txswaphmeolem  20743  xpstopnlem2  20750  ptcmpg  20996  tgplacthmeo  21042  trust  21168  prdsxmslem2  21468  metuval  21488  nghmfval  21647  isnghm  21648  pi1xfrcnv  21974  ismbf1  22456  ismbf  22460  mbfconst  22465  mbfres2  22475  cncombf  22488  deg1val  22919  fta1glem2  22989  fta1g  22990  fta1b  22992  dgrval  23047  dgrlem  23048  coe11  23072  fta1lem  23125  vieta1lem2  23129  ispth  25140  1pthonlem1  25161  constr2spthlem1  25166  2pthlem1  25167  constr2pth  25173  constr3pthlem2  25226  f1o3d  28066  fimacnvinrn  28072  xppreima2  28086  ofpreima  28105  fcnvgreu  28112  fpwrelmapffslem  28157  ordtrest2NEW  28565  qqhval  28614  indf1ofs  28683  esum2dlem  28749  mbfmcst  28917  omssubadd  28958  sitgfval  28999  eulerpartlemgf  29035  orvcval  29113  cvmliftmolem1  29789  cvmliftlem5  29797  cvmliftlem15  29806  cvmlift2lem9a  29811  cvmlift2lem9  29819  ismfs  29972  mthmval  29998  wsuceq123  30281  cnambfre  31693  itg2addnclem2  31698  ftc1anclem1  31721  ftc1anclem6  31726  cdlemg1finvtrlemN  33851  tendoicbv  34069  tendoi  34070  tendoi2  34071  tendoicl  34072  docaffvalN  34398  docafvalN  34399  dihmeetlem1N  34567  dihglblem5apreN  34568  diophrw  35310  rmxfval  35462  rmyfval  35463  aomclem8  35629  cnvtrclfv  35959  frege131d  35999  usgra2pthspth  38434
  Copyright terms: Public domain W3C validator