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

Theorem cnveqd 5740
Description: Equality deduction for converse relation. (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 5738 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
31, 2syl 17 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  ccnv 5548
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-in 3942  df-ss 3951  df-br 5059  df-opab 5121  df-cnv 5557
This theorem is referenced by:  opswap  6080  cores2  6106  fimacnvinrn  6833  nvocnv  7029  2ndval2  7698  2nd1st  7728  cnvf1olem  7796  fparlem3  7800  fparlem4  7801  brtpos2  7889  dftpos4  7902  tpostpos  7903  tposf12  7908  xpcomco  8596  infeq123d  8934  cantnffval2  9147  cnfcomlem  9151  fseqenlem2  9440  dfac12lem1  9558  dfac12r  9561  fpwwe2cbv  10041  fpwwe2lem2  10043  fpwwe2lem6  10046  fpwwe2lem9  10049  fpwwecbv  10055  fpwwelem  10056  funcnvs2  14265  funcnvs3  14266  funcnvs4  14267  relexpcnv  14384  fsumcnv  15118  fprodcnv  15327  bitsf1ocnv  15783  vdwpc  16306  imasval  16774  xpsval  16833  monfval  16992  ismon  16993  monpropd  16997  isepi  17000  invffval  17018  invfval  17019  dfiso2  17032  isofn  17035  oppcinv  17040  isfth  17174  catcisolem  17356  oduval  17730  oduleval  17731  gsumvalx  17876  grpinvcnv  18107  grplactcnv  18142  eqglact  18271  gsumcom2  19026  isunit  19338  issrng  19552  znval  20612  znle2  20630  evpmss  20660  psgnevpmb  20661  ptbasfi  22119  ptval2  22139  ptrescn  22177  xkoptsub  22192  qtopval  22233  txswaphmeolem  22342  ptcmpg  22595  tgplacthmeo  22641  trust  22767  prdsxmslem2  23068  metuval  23088  nghmfval  23260  isnghm  23261  pi1xfrcnv  23590  ismbf1  24154  ismbf  24158  mbfconst  24163  mbfres2  24175  cncombf  24188  deg1val  24619  fta1glem2  24689  fta1g  24690  fta1b  24692  dgrval  24747  dgrlem  24748  coe11  24772  fta1lem  24825  vieta1lem2  24829  ispth  27432  uhgrwkspthlem2  27463  usgr2wlkspthlem1  27466  usgr2wlkspthlem2  27467  pthdlem1  27475  2spthd  27648  3spthd  27883  f1o3d  30301  xppreima2  30324  ofpreima  30339  fcnvgreu  30347  fpwrelmapffslem  30395  tocycfv  30679  tocycf  30687  cycpm2tr  30689  cycpmconjvlem  30711  evpmval  30715  altgnsg  30719  ordtrest2NEW  31066  qqhval  31115  indf1ofs  31185  esum2dlem  31251  mbfmcst  31417  omssubadd  31458  sitgfval  31499  eulerpartlemgf  31537  orvcval  31615  pthhashvtx  32272  cvmliftmolem1  32426  cvmliftlem5  32434  cvmliftlem15  32443  cvmlift2lem9a  32448  cvmlift2lem9  32456  ismfs  32694  mthmval  32720  wsuceq123  32999  cnambfre  34822  itg2addnclem2  34826  ftc1anclem1  34849  ftc1anclem6  34854  dfsymrels2  35663  dfsymrel2  35667  cdlemg1finvtrlemN  37593  tendoicbv  37811  tendoi  37812  tendoi2  37813  tendoicl  37814  docaffvalN  38139  docafvalN  38140  dihmeetlem1N  38308  dihglblem5apreN  38309  diophrw  39236  rmxfval  39381  rmyfval  39382  aomclem8  39541  cnvtrclfv  39949  frege131d  39989  dssmapnvod  40246  smfpimioo  42943  smfpimcc  42963  smfsuplem2  42967
  Copyright terms: Public domain W3C validator