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

Theorem cnveqd 5205
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 5203 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
31, 2syl 17 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  ccnv 5024
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-in 3543  df-ss 3550  df-br 4575  df-opab 4635  df-cnv 5033
This theorem is referenced by:  cnvsng  5522  opswap  5523  cores2  5548  fimacnvinrn  6238  nvocnv  6412  2ndval2  7051  2nd1st  7078  cnvf1olem  7136  fparlem3  7140  fparlem4  7141  brtpos2  7219  dftpos4  7232  tpostpos  7233  tposf12  7238  xpcomco  7909  infeq123d  8244  cantnffval2  8449  cnfcomlem  8453  fseqenlem2  8705  dfac12lem1  8822  dfac12r  8825  fpwwe2cbv  9305  fpwwe2lem2  9307  fpwwe2lem6  9310  fpwwe2lem9  9313  fpwwecbv  9319  fpwwelem  9320  funcnvs2  13451  funcnvs3  13452  funcnvs4  13453  relexpcnv  13566  fsumcnv  14289  fprodcnv  14495  bitsf1ocnv  14947  vdwpc  15465  imasval  15937  xpsfval  15993  xpsval  15998  monfval  16158  ismon  16159  monpropd  16163  isepi  16166  invffval  16184  invfval  16185  dfiso2  16198  isofn  16201  oppcinv  16206  isfth  16340  catcisolem  16522  oduval  16896  oduleval  16897  gsumvalx  17036  grpinvcnv  17249  grplactcnv  17284  eqglact  17411  gsumcom2  18140  isunit  18423  issrng  18616  znval  19644  znle2  19663  evpmss  19693  psgnevpmb  19694  ptbasfi  21133  ptval2  21153  ptrescn  21191  xkoptsub  21206  qtopval  21247  txswaphmeolem  21356  xpstopnlem2  21363  ptcmpg  21610  tgplacthmeo  21656  trust  21782  prdsxmslem2  22082  metuval  22102  nghmfval  22265  isnghm  22266  pi1xfrcnv  22593  ismbf1  23113  ismbf  23117  mbfconst  23122  mbfres2  23132  cncombf  23145  deg1val  23574  fta1glem2  23644  fta1g  23645  fta1b  23647  dgrval  23702  dgrlem  23703  coe11  23727  fta1lem  23780  vieta1lem2  23784  ispth  25861  1pthonlem1  25882  constr2spthlem1  25887  2pthlem1  25888  constr2pth  25894  constr3pthlem2  25947  f1o3d  28616  xppreima2  28633  ofpreima  28651  fcnvgreu  28658  fpwrelmapffslem  28698  ordtrest2NEW  29100  qqhval  29149  indf1ofs  29218  esum2dlem  29284  mbfmcst  29451  omssubadd  29492  sitgfval  29533  eulerpartlemgf  29571  orvcval  29649  cvmliftmolem1  30320  cvmliftlem5  30328  cvmliftlem15  30337  cvmlift2lem9a  30342  cvmlift2lem9  30350  ismfs  30503  mthmval  30529  wsuceq123  30807  cnambfre  32428  itg2addnclem2  32432  ftc1anclem1  32455  ftc1anclem6  32460  cdlemg1finvtrlemN  34681  tendoicbv  34899  tendoi  34900  tendoi2  34901  tendoicl  34902  docaffvalN  35228  docafvalN  35229  dihmeetlem1N  35397  dihglblem5apreN  35398  diophrw  36140  rmxfval  36286  rmyfval  36287  aomclem8  36449  cnvtrclfv  36835  frege131d  36875  dssmapnvod  37134  smfpimioo  39473  isPth  40928  uhgr1wlkspthlem2  40959  usgr2wlkspthlem1  40962  usgr2wlkspthlem2  40963  pthdlem1  40971  2spthd  41147  3spthd  41342
  Copyright terms: Public domain W3C validator