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

Theorem cnveq 5727
Description: Equality theorem for converse relation. (Contributed by NM, 13-Aug-1995.)
Assertion
Ref Expression
cnveq (𝐴 = 𝐵𝐴 = 𝐵)

Proof of Theorem cnveq
StepHypRef Expression
1 cnvss 5726 . . 3 (𝐴𝐵𝐴𝐵)
2 cnvss 5726 . . 3 (𝐵𝐴𝐵𝐴)
31, 2anim12i 615 . 2 ((𝐴𝐵𝐵𝐴) → (𝐴𝐵𝐵𝐴))
4 eqss 3966 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
5 eqss 3966 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
63, 4, 53imtr4i 295 1 (𝐴 = 𝐵𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wss 3918  ccnv 5537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-v 3481  df-in 3925  df-ss 3935  df-br 5050  df-opab 5112  df-cnv 5546
This theorem is referenced by:  cnveqi  5728  cnveqd  5729  rneq  5789  cnveqb  6036  predeq123  6132  f1eq1  6553  f1ssf1  6629  f1o00  6632  foeqcnvco  7040  funcnvuni  7621  tposfn2  7899  ereq1  8281  infeq3  8930  1arith  16252  vdwmc  16303  vdwnnlem1  16320  ramub2  16339  rami  16340  isps  17803  istsr  17818  isdir  17833  isrim0  19466  psrbag  20132  psrbaglefi  20140  iscn  21831  ishmeo  22355  symgtgp  22702  ustincl  22804  ustdiag  22805  ustinvel  22806  ustexhalf  22807  ustexsym  22812  ust0  22816  isi1f  24269  itg1val  24278  fta1lem  24894  fta1  24895  vieta1lem2  24898  vieta1  24899  sqff1o  25758  istrl  27477  isspth  27504  upgrwlkdvspth  27519  uhgrwkspthlem1  27533  0spth  27902  nlfnval  29655  padct  30454  tocyc01  30780  cycpmconjslem2  30817  indf1ofs  31305  ismbfm  31530  issibf  31611  sitgfval  31619  eulerpartlemelr  31635  eulerpartleme  31641  eulerpartlemo  31643  eulerpartlemt0  31647  eulerpartlemt  31649  eulerpartgbij  31650  eulerpartlemr  31652  eulerpartlemgs2  31658  eulerpartlemn  31659  eulerpart  31660  funen1cnv  32377  iscvm  32526  elmpst  32803  elsymrels2  35854  elsymrels4  35856  symreleq  35859  elrefsymrels2  35870  eleqvrels2  35892  eldisjs  36020  lkrval  36289  ltrncnvnid  37328  cdlemkuu  38096  pw2f1o2val  39827  pwfi2f1o  39887  clcnvlem  40170  rfovcnvf1od  40553  fsovrfovd  40558  issmflem  43218  isrngisom  44377
  Copyright terms: Public domain W3C validator