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

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

Proof of Theorem cnveq
StepHypRef Expression
1 cnvss 5200 . . 3 (𝐴𝐵𝐴𝐵)
2 cnvss 5200 . . 3 (𝐵𝐴𝐵𝐴)
31, 2anim12i 587 . 2 ((𝐴𝐵𝐵𝐴) → (𝐴𝐵𝐵𝐴))
4 eqss 3578 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
5 eqss 3578 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
63, 4, 53imtr4i 279 1 (𝐴 = 𝐵𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wss 3535  ccnv 5023
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
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 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-in 3542  df-ss 3549  df-br 4574  df-opab 4634  df-cnv 5032
This theorem is referenced by:  cnveqi  5203  cnveqd  5204  rneq  5255  cnveqb  5490  predeq123  5580  f1eq1  5990  f1o00  6064  foeqcnvco  6429  funcnvuni  6985  tposfn2  7234  ereq1  7609  infeq3  8242  1arith  15411  vdwmc  15462  vdwnnlem1  15479  ramub2  15498  rami  15499  isps  16967  istsr  16982  isdir  16997  isrim0  18488  psrbag  19127  psrbaglefi  19135  iscn  20787  ishmeo  21310  symgtgp  21653  ustincl  21759  ustdiag  21760  ustinvel  21761  ustexhalf  21762  ustexsym  21767  ust0  21771  isi1f  23160  itg1val  23169  fta1lem  23779  fta1  23780  vieta1lem2  23783  vieta1  23784  sqff1o  24621  istrl  25829  isspth  25861  0spth  25863  nlfnval  27926  padct  28687  indf1ofs  29217  ismbfm  29443  issibf  29524  sitgfval  29532  eulerpartlemelr  29548  eulerpartleme  29554  eulerpartlemo  29556  eulerpartlemt0  29560  eulerpartlemt  29562  eulerpartgbij  29563  eulerpartlemr  29565  eulerpartlemgs2  29571  eulerpartlemn  29572  eulerpart  29573  iscvm  30297  elmpst  30489  lkrval  33192  ltrncnvnid  34230  cdlemkuu  35000  pw2f1o2val  36423  pwfi2f1o  36483  clcnvlem  36748  rfovcnvf1od  37117  fsovrfovd  37122  issmflem  39413  f1ssf1  40143  isTrl  40902  issPth  40928  upgrwlkdvspth  40943  uhgr1wlkspthlem1  40957  0spth-av  41292  isrngisom  41684
  Copyright terms: Public domain W3C validator