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

Theorem cnveq 4979
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 4978 . . 3  |-  ( A 
C_  B  ->  `' A  C_  `' B )
2 cnvss 4978 . . 3  |-  ( B 
C_  A  ->  `' B  C_  `' A )
31, 2anim12i 550 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( `' A  C_  `' B  /\  `' B  C_  `' A ) )
4 eqss 3299 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3299 . 2  |-  ( `' A  =  `' B  <->  ( `' A  C_  `' B  /\  `' B  C_  `' A
) )
63, 4, 53imtr4i 258 1  |-  ( A  =  B  ->  `' A  =  `' B
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    C_ wss 3256   `'ccnv 4810
This theorem is referenced by:  cnveqi  4980  cnveqd  4981  rneq  5028  cnveqb  5259  funcnvuni  5451  f1eq1  5567  f1o00  5643  foeqcnvco  5959  tposfn2  6430  ereq1  6841  wemapso2  7447  cantnfs  7547  oemapso  7564  mapfien  7579  1arith  13215  vdwmc  13266  vdwnnlem1  13283  ramub2  13302  rami  13303  isps  14554  istsr  14569  isdir  14597  dprdw  15488  psrbag  16351  psrbaglefi  16357  mplelbas  16414  mplsubglem  16418  mpllsslem  16419  ltbwe  16453  iscn  17214  ishmeo  17705  symgtgp  18045  ustincl  18151  ustdiag  18152  ustinvel  18153  ustexhalf  18154  ustexsym  18159  ust0  18163  isi1f  19426  itg1val  19435  mdegval  19846  fta1lem  20084  fta1  20085  vieta1lem2  20088  vieta1  20089  sqff1o  20825  istrl  21394  isspth  21416  0spth  21418  nlfnval  23225  indf1ofs  24212  ismbfm  24389  iscvm  24718  predeq1  25186  pw2f1o2val  26794  frlmelbas  26886  frlmssuvc1  26908  frlmssuvc2  26909  frlmsslsp  26910  ellspd  26916  pwfi2f1o  26922  islindf4  26970  lkrval  29254  ltrncnvnid  30292  cdlemkuu  31060
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-in 3263  df-ss 3270  df-br 4147  df-opab 4201  df-cnv 4819
  Copyright terms: Public domain W3C validator