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

Theorem cnveq 4855
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 4854 . . 3  |-  ( A 
C_  B  ->  `' A  C_  `' B )
2 cnvss 4854 . . 3  |-  ( B 
C_  A  ->  `' B  C_  `' A )
31, 2anim12i 549 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( `' A  C_  `' B  /\  `' B  C_  `' A ) )
4 eqss 3194 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3194 . 2  |-  ( `' A  =  `' B  <->  ( `' A  C_  `' B  /\  `' B  C_  `' A
) )
63, 4, 53imtr4i 257 1  |-  ( A  =  B  ->  `' A  =  `' B
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623    C_ wss 3152   `'ccnv 4688
This theorem is referenced by:  cnveqi  4856  cnveqd  4857  rneq  4904  cnveqb  5129  funcnvuni  5317  f1eq1  5432  f1o00  5508  foeqcnvco  5804  tposfn2  6256  ereq1  6667  wemapso2  7267  cantnfs  7367  oemapso  7384  mapfien  7399  1arith  12974  vdwmc  13025  vdwnnlem1  13042  ramub2  13061  rami  13062  isps  14311  istsr  14326  isdir  14354  dprdw  15245  psrbag  16112  psrbaglefi  16118  mplelbas  16175  mplsubglem  16179  mpllsslem  16180  ltbwe  16214  iscn  16965  ishmeo  17450  symgtgp  17784  isi1f  19029  itg1val  19038  mdegval  19449  fta1lem  19687  fta1  19688  vieta1lem2  19691  vieta1  19692  sqff1o  20420  nlfnval  22461  iscvm  23201  predeq1  23580  nfwval  24657  pw2f1o2val  26544  frlmelbas  26636  frlmssuvc1  26658  frlmssuvc2  26659  frlmsslsp  26660  ellspd  26666  pwfi2f1o  26672  islindf4  26720  lkrval  28651  ltrncnvnid  29689  cdlemkuu  30457
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-in 3159  df-ss 3166  df-br 4024  df-opab 4078  df-cnv 4697
  Copyright terms: Public domain W3C validator