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

Theorem cnveq 5038
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 5037 . . 3  |-  ( A 
C_  B  ->  `' A  C_  `' B )
2 cnvss 5037 . . 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 3355 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3355 . 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 1652    C_ wss 3312   `'ccnv 4869
This theorem is referenced by:  cnveqi  5039  cnveqd  5040  rneq  5087  cnveqb  5318  funcnvuni  5510  f1eq1  5626  f1o00  5702  foeqcnvco  6019  tposfn2  6493  ereq1  6904  wemapso2  7513  cantnfs  7613  oemapso  7630  mapfien  7645  1arith  13287  vdwmc  13338  vdwnnlem1  13355  ramub2  13374  rami  13375  isps  14626  istsr  14641  isdir  14669  dprdw  15560  psrbag  16423  psrbaglefi  16429  mplelbas  16486  mplsubglem  16490  mpllsslem  16491  ltbwe  16525  iscn  17291  ishmeo  17783  symgtgp  18123  ustincl  18229  ustdiag  18230  ustinvel  18231  ustexhalf  18232  ustexsym  18237  ust0  18241  isi1f  19558  itg1val  19567  mdegval  19978  fta1lem  20216  fta1  20217  vieta1lem2  20220  vieta1  20221  sqff1o  20957  istrl  21529  isspth  21561  0spth  21563  nlfnval  23376  indf1ofs  24415  ismbfm  24594  issibf  24640  sitgfval  24647  iscvm  24938  predeq123  25432  wlimeq12  25562  pw2f1o2val  27101  frlmelbas  27192  frlmssuvc1  27214  frlmssuvc2  27215  frlmsslsp  27216  ellspd  27222  pwfi2f1o  27228  islindf4  27276  lkrval  29823  ltrncnvnid  30861  cdlemkuu  31629
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-in 3319  df-ss 3326  df-br 4205  df-opab 4259  df-cnv 4878
  Copyright terms: Public domain W3C validator