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

Theorem cnveqd 5499
Description: Equality deduction for converse. (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 5497 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
31, 2syl 17 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  ccnv 5310
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-in 3776  df-ss 3783  df-br 4845  df-opab 4907  df-cnv 5319
This theorem is referenced by:  cnvsngOLD  5835  opswap  5836  cores2  5862  fimacnvinrn  6566  nvocnv  6757  2ndval2  7412  2nd1st  7441  cnvf1olem  7505  fparlem3  7509  fparlem4  7510  brtpos2  7589  dftpos4  7602  tpostpos  7603  tposf12  7608  xpcomco  8285  infeq123d  8622  cantnffval2  8835  cnfcomlem  8839  fseqenlem2  9127  dfac12lem1  9246  dfac12r  9249  fpwwe2cbv  9733  fpwwe2lem2  9735  fpwwe2lem6  9738  fpwwe2lem9  9741  fpwwecbv  9747  fpwwelem  9748  funcnvs2  13878  funcnvs3  13879  funcnvs4  13880  relexpcnv  13994  fsumcnv  14723  fprodcnv  14930  bitsf1ocnv  15381  vdwpc  15897  imasval  16372  xpsfval  16428  xpsval  16433  monfval  16592  ismon  16593  monpropd  16597  isepi  16600  invffval  16618  invfval  16619  dfiso2  16632  isofn  16635  oppcinv  16640  isfth  16774  catcisolem  16956  oduval  17331  oduleval  17332  gsumvalx  17471  grpinvcnv  17684  grplactcnv  17719  eqglact  17843  gsumcom2  18571  isunit  18855  issrng  19050  znval  20087  znle2  20105  evpmss  20135  psgnevpmb  20136  ptbasfi  21595  ptval2  21615  ptrescn  21653  xkoptsub  21668  qtopval  21709  txswaphmeolem  21818  xpstopnlem2  21825  ptcmpg  22071  tgplacthmeo  22117  trust  22243  prdsxmslem2  22544  metuval  22564  nghmfval  22736  isnghm  22737  pi1xfrcnv  23066  ismbf1  23604  ismbf  23608  mbfconst  23613  mbfres2  23625  cncombf  23638  deg1val  24069  fta1glem2  24139  fta1g  24140  fta1b  24142  dgrval  24197  dgrlem  24198  coe11  24222  fta1lem  24275  vieta1lem2  24279  ispth  26846  uhgrwkspthlem2  26877  usgr2wlkspthlem1  26880  usgr2wlkspthlem2  26881  pthdlem1  26889  2spthd  27080  3spthd  27348  f1o3d  29757  xppreima2  29776  ofpreima  29791  fcnvgreu  29798  fpwrelmapffslem  29833  ordtrest2NEW  30293  qqhval  30342  indf1ofs  30412  esum2dlem  30478  mbfmcst  30645  omssubadd  30686  sitgfval  30727  eulerpartlemgf  30765  orvcval  30843  cvmliftmolem1  31584  cvmliftlem5  31592  cvmliftlem15  31601  cvmlift2lem9a  31606  cvmlift2lem9  31614  ismfs  31767  mthmval  31793  wsuceq123  32078  cnambfre  33768  itg2addnclem2  33772  ftc1anclem1  33795  ftc1anclem6  33800  dfsymrels2  34602  dfsymrel2  34606  cdlemg1finvtrlemN  36353  tendoicbv  36571  tendoi  36572  tendoi2  36573  tendoicl  36574  docaffvalN  36899  docafvalN  36900  dihmeetlem1N  37068  dihglblem5apreN  37069  diophrw  37821  rmxfval  37967  rmyfval  37968  aomclem8  38129  cnvtrclfv  38513  frege131d  38553  dssmapnvod  38811  smfpimioo  41473  smfpimcc  41493  smfsuplem2  41497
  Copyright terms: Public domain W3C validator