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

Theorem cnveqd 5287
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 5285 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
31, 2syl 17 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481  ccnv 5103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-in 3574  df-ss 3581  df-br 4645  df-opab 4704  df-cnv 5112
This theorem is referenced by:  cnvsng  5609  opswap  5610  cores2  5636  fimacnvinrn  6334  nvocnv  6522  2ndval2  7171  2nd1st  7198  cnvf1olem  7260  fparlem3  7264  fparlem4  7265  brtpos2  7343  dftpos4  7356  tpostpos  7357  tposf12  7362  xpcomco  8035  infeq123d  8372  cantnffval2  8577  cnfcomlem  8581  fseqenlem2  8833  dfac12lem1  8950  dfac12r  8953  fpwwe2cbv  9437  fpwwe2lem2  9439  fpwwe2lem6  9442  fpwwe2lem9  9445  fpwwecbv  9451  fpwwelem  9452  funcnvs2  13639  funcnvs3  13640  funcnvs4  13641  relexpcnv  13756  fsumcnv  14485  fprodcnv  14694  bitsf1ocnv  15147  vdwpc  15665  imasval  16152  xpsfval  16208  xpsval  16213  monfval  16373  ismon  16374  monpropd  16378  isepi  16381  invffval  16399  invfval  16400  dfiso2  16413  isofn  16416  oppcinv  16421  isfth  16555  catcisolem  16737  oduval  17111  oduleval  17112  gsumvalx  17251  grpinvcnv  17464  grplactcnv  17499  eqglact  17626  gsumcom2  18355  isunit  18638  issrng  18831  znval  19864  znle2  19883  evpmss  19913  psgnevpmb  19914  ptbasfi  21365  ptval2  21385  ptrescn  21423  xkoptsub  21438  qtopval  21479  txswaphmeolem  21588  xpstopnlem2  21595  ptcmpg  21842  tgplacthmeo  21888  trust  22014  prdsxmslem2  22315  metuval  22335  nghmfval  22507  isnghm  22508  pi1xfrcnv  22838  ismbf1  23374  ismbf  23378  mbfconst  23383  mbfres2  23393  cncombf  23406  deg1val  23837  fta1glem2  23907  fta1g  23908  fta1b  23910  dgrval  23965  dgrlem  23966  coe11  23990  fta1lem  24043  vieta1lem2  24047  ispth  26600  uhgrwkspthlem2  26631  usgr2wlkspthlem1  26634  usgr2wlkspthlem2  26635  pthdlem1  26643  2spthd  26818  3spthd  27016  f1o3d  29404  xppreima2  29423  ofpreima  29439  fcnvgreu  29446  fpwrelmapffslem  29481  ordtrest2NEW  29943  qqhval  29992  indf1ofs  30062  esum2dlem  30128  mbfmcst  30295  omssubadd  30336  sitgfval  30377  eulerpartlemgf  30415  orvcval  30493  cvmliftmolem1  31237  cvmliftlem5  31245  cvmliftlem15  31254  cvmlift2lem9a  31259  cvmlift2lem9  31267  ismfs  31420  mthmval  31446  wsuceq123  31734  cnambfre  33429  itg2addnclem2  33433  ftc1anclem1  33456  ftc1anclem6  33461  cdlemg1finvtrlemN  35682  tendoicbv  35900  tendoi  35901  tendoi2  35902  tendoicl  35903  docaffvalN  36229  docafvalN  36230  dihmeetlem1N  36398  dihglblem5apreN  36399  diophrw  37141  rmxfval  37287  rmyfval  37288  aomclem8  37450  cnvtrclfv  37835  frege131d  37875  dssmapnvod  38134  smfpimioo  40757  smfpimcc  40777  smfsuplem2  40781
  Copyright terms: Public domain W3C validator