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

Theorem cnveqd 5330
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 5328 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
31, 2syl 17 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  ccnv 5142
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-in 3614  df-ss 3621  df-br 4686  df-opab 4746  df-cnv 5151
This theorem is referenced by:  cnvsngOLD  5659  opswap  5660  cores2  5686  fimacnvinrn  6388  nvocnv  6577  2ndval2  7228  2nd1st  7257  cnvf1olem  7320  fparlem3  7324  fparlem4  7325  brtpos2  7403  dftpos4  7416  tpostpos  7417  tposf12  7422  xpcomco  8091  infeq123d  8428  cantnffval2  8630  cnfcomlem  8634  fseqenlem2  8886  dfac12lem1  9003  dfac12r  9006  fpwwe2cbv  9490  fpwwe2lem2  9492  fpwwe2lem6  9495  fpwwe2lem9  9498  fpwwecbv  9504  fpwwelem  9505  funcnvs2  13704  funcnvs3  13705  funcnvs4  13706  relexpcnv  13819  fsumcnv  14548  fprodcnv  14757  bitsf1ocnv  15213  vdwpc  15731  imasval  16218  xpsfval  16274  xpsval  16279  monfval  16439  ismon  16440  monpropd  16444  isepi  16447  invffval  16465  invfval  16466  dfiso2  16479  isofn  16482  oppcinv  16487  isfth  16621  catcisolem  16803  oduval  17177  oduleval  17178  gsumvalx  17317  grpinvcnv  17530  grplactcnv  17565  eqglact  17692  gsumcom2  18420  isunit  18703  issrng  18898  znval  19931  znle2  19950  evpmss  19980  psgnevpmb  19981  ptbasfi  21432  ptval2  21452  ptrescn  21490  xkoptsub  21505  qtopval  21546  txswaphmeolem  21655  xpstopnlem2  21662  ptcmpg  21908  tgplacthmeo  21954  trust  22080  prdsxmslem2  22381  metuval  22401  nghmfval  22573  isnghm  22574  pi1xfrcnv  22903  ismbf1  23438  ismbf  23442  mbfconst  23447  mbfres2  23457  cncombf  23470  deg1val  23901  fta1glem2  23971  fta1g  23972  fta1b  23974  dgrval  24029  dgrlem  24030  coe11  24054  fta1lem  24107  vieta1lem2  24111  ispth  26675  uhgrwkspthlem2  26706  usgr2wlkspthlem1  26709  usgr2wlkspthlem2  26710  pthdlem1  26718  2spthd  26906  3spthd  27154  f1o3d  29559  xppreima2  29578  ofpreima  29593  fcnvgreu  29600  fpwrelmapffslem  29635  ordtrest2NEW  30097  qqhval  30146  indf1ofs  30216  esum2dlem  30282  mbfmcst  30449  omssubadd  30490  sitgfval  30531  eulerpartlemgf  30569  orvcval  30647  cvmliftmolem1  31389  cvmliftlem5  31397  cvmliftlem15  31406  cvmlift2lem9a  31411  cvmlift2lem9  31419  ismfs  31572  mthmval  31598  wsuceq123  31884  cnambfre  33588  itg2addnclem2  33592  ftc1anclem1  33615  ftc1anclem6  33620  dfsymrels2  34431  dfsymrel2  34435  cdlemg1finvtrlemN  36180  tendoicbv  36398  tendoi  36399  tendoi2  36400  tendoicl  36401  docaffvalN  36727  docafvalN  36728  dihmeetlem1N  36896  dihglblem5apreN  36897  diophrw  37639  rmxfval  37785  rmyfval  37786  aomclem8  37948  cnvtrclfv  38333  frege131d  38373  dssmapnvod  38631  smfpimioo  41315  smfpimcc  41335  smfsuplem2  41339
  Copyright terms: Public domain W3C validator