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

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

Proof of Theorem cnveq
StepHypRef Expression
1 cnvss 5180 . . 3
2 cnvss 5180 . . 3
31, 2anim12i 566 . 2
4 eqss 3518 . 2
5 eqss 3518 . 2
63, 4, 53imtr4i 266 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  C_wss 3475  `'ccnv 5003
This theorem is referenced by:  cnveqi  5182  cnveqd  5183  rneq  5233  cnveqb  5467  f1eq1  5781  f1o00  5853  foeqcnvco  6203  funcnvuni  6753  tposfn2  6996  ereq1  7337  wemapso2OLD  7998  cantnfsOLD  8136  mapfienOLD  8159  1arith  14445  vdwmc  14496  vdwnnlem1  14513  ramub2  14532  rami  14533  isps  15832  istsr  15847  isdir  15862  dprdwOLD  17050  isrim0  17372  psrbag  18013  psrbaglefi  18023  psrbaglefiOLD  18024  mplelbasOLD  18089  mplsubglemOLD  18095  mpllsslemOLD  18096  frlmelbasOLD  18789  frlmssuvc1OLD  18827  frlmssuvc2OLD  18828  frlmsslspOLD  18830  ellspdOLD  18837  iscn  19736  ishmeo  20260  symgtgp  20600  ustincl  20710  ustdiag  20711  ustinvel  20712  ustexhalf  20713  ustexsym  20718  ust0  20722  isi1f  22081  itg1val  22090  mdegvalOLD  22463  fta1lem  22703  fta1  22704  vieta1lem2  22707  vieta1  22708  sqff1o  23456  istrl  24539  isspth  24571  0spth  24573  nlfnval  26800  indf1ofs  28039  ismbfm  28223  issibf  28275  sitgfval  28283  eulerpartlemelr  28296  eulerpartleme  28302  eulerpartlemo  28304  eulerpartlemt0  28308  eulerpartlemt  28310  eulerpartgbij  28311  eulerpartlemr  28313  eulerpartlemgs2  28319  eulerpartlemn  28320  eulerpart  28321  iscvm  28704  elmpst  28896  predeq123  29245  wlimeq12  29375  pw2f1o2val  30981  pwfi2f1o  31044  isrngisom  32702  lkrval  34813  ltrncnvnid  35851  cdlemkuu  36621
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-in 3482  df-ss 3489  df-br 4453  df-opab 4511  df-cnv 5012
  Copyright terms: Public domain W3C validator