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

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

Proof of Theorem cnveq
StepHypRef Expression
1 cnvss 5451 . . 3 (𝐴𝐵𝐴𝐵)
2 cnvss 5451 . . 3 (𝐵𝐴𝐵𝐴)
31, 2anim12i 591 . 2 ((𝐴𝐵𝐵𝐴) → (𝐴𝐵𝐵𝐴))
4 eqss 3760 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
5 eqss 3760 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
63, 4, 53imtr4i 281 1 (𝐴 = 𝐵𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1632  wss 3716  ccnv 5266
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-in 3723  df-ss 3730  df-br 4806  df-opab 4866  df-cnv 5275
This theorem is referenced by:  cnveqi  5453  cnveqd  5454  rneq  5507  cnveqb  5749  predeq123  5843  f1eq1  6258  f1ssf1  6331  f1o00  6334  foeqcnvco  6720  funcnvuni  7286  tposfn2  7545  ereq1  7921  infeq3  8554  1arith  15854  vdwmc  15905  vdwnnlem1  15922  ramub2  15941  rami  15942  isps  17424  istsr  17439  isdir  17454  isrim0  18946  psrbag  19587  psrbaglefi  19595  iscn  21262  ishmeo  21785  symgtgp  22127  ustincl  22233  ustdiag  22234  ustinvel  22235  ustexhalf  22236  ustexsym  22241  ust0  22245  isi1f  23661  itg1val  23670  fta1lem  24282  fta1  24283  vieta1lem2  24286  vieta1  24287  sqff1o  25129  istrl  26825  isspth  26852  upgrwlkdvspth  26867  uhgrwkspthlem1  26881  0spth  27300  nlfnval  29071  padct  29828  indf1ofs  30419  ismbfm  30645  issibf  30726  sitgfval  30734  eulerpartlemelr  30750  eulerpartleme  30756  eulerpartlemo  30758  eulerpartlemt0  30762  eulerpartlemt  30764  eulerpartgbij  30765  eulerpartlemr  30767  eulerpartlemgs2  30773  eulerpartlemn  30774  eulerpart  30775  iscvm  31570  elmpst  31762  elsymrels2  34641  elsymrels4  34643  symreleq  34646  elrefsymrels2  34657  lkrval  34897  ltrncnvnid  35935  cdlemkuu  36704  pw2f1o2val  38127  pwfi2f1o  38187  clcnvlem  38451  rfovcnvf1od  38819  fsovrfovd  38824  issmflem  41461  isrngisom  42425
  Copyright terms: Public domain W3C validator