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

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

Proof of Theorem cnveq
StepHypRef Expression
1 cnvss 5829 . . 3 (𝐴𝐵𝐴𝐵)
2 cnvss 5829 . . 3 (𝐵𝐴𝐵𝐴)
31, 2anim12i 614 . 2 ((𝐴𝐵𝐵𝐴) → (𝐴𝐵𝐵𝐴))
4 eqss 3960 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
5 eqss 3960 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
63, 4, 53imtr4i 292 1 (𝐴 = 𝐵𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wss 3911  ccnv 5633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3446  df-in 3918  df-ss 3928  df-br 5107  df-opab 5169  df-cnv 5642
This theorem is referenced by:  cnveqi  5831  cnveqd  5832  rneq  5892  cnveqb  6149  predeq123  6255  f1eq1  6734  f1ssf1  6817  f1o00  6820  foeqcnvco  7247  funcnvuni  7869  tposfn2  8180  ereq1  8658  cnvfi  9127  infeq3  9421  1arith  16804  vdwmc  16855  vdwnnlem1  16872  ramub2  16891  rami  16892  isps  18462  istsr  18477  isdir  18492  isrim0OLD  20161  isrim0  20163  psrbag  21335  psrbaglefi  21350  psrbaglefiOLD  21351  iscn  22602  ishmeo  23126  symgtgp  23473  ustincl  23575  ustdiag  23576  ustinvel  23577  ustexhalf  23578  ustexsym  23583  ust0  23587  isi1f  25054  itg1val  25063  fta1lem  25683  fta1  25684  vieta1lem2  25687  vieta1  25688  sqff1o  26547  istrl  28686  isspth  28714  upgrwlkdvspth  28729  uhgrwkspthlem1  28743  0spth  29112  nlfnval  30865  padct  31683  tocyc01  32016  cycpmconjslem2  32053  indf1ofs  32682  ismbfm  32907  issibf  32990  sitgfval  32998  eulerpartlemelr  33014  eulerpartleme  33020  eulerpartlemo  33022  eulerpartlemt0  33026  eulerpartlemt  33028  eulerpartgbij  33029  eulerpartlemr  33031  eulerpartlemgs2  33037  eulerpartlemn  33038  eulerpart  33039  funen1cnv  33749  iscvm  33910  elmpst  34187  elsymrels2  37061  elsymrels4  37063  symreleq  37066  elrefsymrels2  37077  eleqvrels2  37100  eldisjs  37230  lkrval  37596  ltrncnvnid  38636  cdlemkuu  39404  pw2f1o2val  41406  pwfi2f1o  41466  clcnvlem  41983  rfovcnvf1od  42364  fsovrfovd  42369  issmflem  45054  isrngisom  46280
  Copyright terms: Public domain W3C validator