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

Theorem cnveq 5166
Description: Equality theorem for converse. (Contributed by NM, 13-Aug-1995.)
Assertion
Ref Expression
cnveq  |-  ( A  =  B  ->  `' A  =  `' B
)

Proof of Theorem cnveq
StepHypRef Expression
1 cnvss 5165 . . 3  |-  ( A 
C_  B  ->  `' A  C_  `' B )
2 cnvss 5165 . . 3  |-  ( B 
C_  A  ->  `' B  C_  `' A )
31, 2anim12i 566 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( `' A  C_  `' B  /\  `' B  C_  `' A ) )
4 eqss 3504 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3504 . 2  |-  ( `' A  =  `' B  <->  ( `' A  C_  `' B  /\  `' B  C_  `' A
) )
63, 4, 53imtr4i 266 1  |-  ( A  =  B  ->  `' A  =  `' B
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1383    C_ wss 3461   `'ccnv 4988
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-in 3468  df-ss 3475  df-br 4438  df-opab 4496  df-cnv 4997
This theorem is referenced by:  cnveqi  5167  cnveqd  5168  rneq  5218  cnveqb  5452  f1eq1  5766  f1o00  5838  foeqcnvco  6188  funcnvuni  6738  tposfn2  6979  ereq1  7320  wemapso2OLD  7980  cantnfsOLD  8118  mapfienOLD  8141  1arith  14427  vdwmc  14478  vdwnnlem1  14495  ramub2  14514  rami  14515  isps  15811  istsr  15826  isdir  15841  dprdwOLD  17029  isrim0  17351  psrbag  17992  psrbaglefi  18002  psrbaglefiOLD  18003  mplelbasOLD  18068  mplsubglemOLD  18074  mpllsslemOLD  18075  frlmelbasOLD  18767  frlmssuvc1OLD  18805  frlmssuvc2OLD  18806  frlmsslspOLD  18808  ellspdOLD  18815  iscn  19714  ishmeo  20238  symgtgp  20578  ustincl  20688  ustdiag  20689  ustinvel  20690  ustexhalf  20691  ustexsym  20696  ust0  20700  isi1f  22059  itg1val  22068  mdegvalOLD  22441  fta1lem  22681  fta1  22682  vieta1lem2  22685  vieta1  22686  sqff1o  23434  istrl  24517  isspth  24549  0spth  24551  nlfnval  26778  indf1ofs  28017  ismbfm  28201  issibf  28253  sitgfval  28261  eulerpartlemelr  28274  eulerpartleme  28280  eulerpartlemo  28282  eulerpartlemt0  28286  eulerpartlemt  28288  eulerpartgbij  28289  eulerpartlemr  28291  eulerpartlemgs2  28297  eulerpartlemn  28298  eulerpart  28299  iscvm  28682  elmpst  28874  predeq123  29221  wlimeq12  29351  pw2f1o2val  30957  pwfi2f1o  31020  isrngisom  32537  lkrval  34688  ltrncnvnid  35726  cdlemkuu  36496
  Copyright terms: Public domain W3C validator