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

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

Proof of Theorem cnveq
StepHypRef Expression
1 cnvss 5283 . . 3 (𝐴𝐵𝐴𝐵)
2 cnvss 5283 . . 3 (𝐵𝐴𝐵𝐴)
31, 2anim12i 589 . 2 ((𝐴𝐵𝐵𝐴) → (𝐴𝐵𝐵𝐴))
4 eqss 3610 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
5 eqss 3610 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
63, 4, 53imtr4i 281 1 (𝐴 = 𝐵𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1481  wss 3567  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:  cnveqi  5286  cnveqd  5287  rneq  5340  cnveqb  5578  predeq123  5669  f1eq1  6083  f1ssf1  6155  f1o00  6158  foeqcnvco  6540  funcnvuni  7104  tposfn2  7359  ereq1  7734  infeq3  8371  1arith  15612  vdwmc  15663  vdwnnlem1  15680  ramub2  15699  rami  15700  isps  17183  istsr  17198  isdir  17213  isrim0  18704  psrbag  19345  psrbaglefi  19353  iscn  21020  ishmeo  21543  symgtgp  21886  ustincl  21992  ustdiag  21993  ustinvel  21994  ustexhalf  21995  ustexsym  22000  ust0  22004  isi1f  23422  itg1val  23431  fta1lem  24043  fta1  24044  vieta1lem2  24047  vieta1  24048  sqff1o  24889  istrl  26574  isspth  26601  upgrwlkdvspth  26616  uhgrwkspthlem1  26630  0spth  26967  nlfnval  28710  padct  29471  indf1ofs  30062  ismbfm  30288  issibf  30369  sitgfval  30377  eulerpartlemelr  30393  eulerpartleme  30399  eulerpartlemo  30401  eulerpartlemt0  30405  eulerpartlemt  30407  eulerpartgbij  30408  eulerpartlemr  30410  eulerpartlemgs2  30416  eulerpartlemn  30417  eulerpart  30418  iscvm  31215  elmpst  31407  lkrval  34194  ltrncnvnid  35232  cdlemkuu  36002  pw2f1o2val  37425  pwfi2f1o  37485  clcnvlem  37749  rfovcnvf1od  38118  fsovrfovd  38123  issmflem  40699  isrngisom  41661
  Copyright terms: Public domain W3C validator