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

Theorem cnveq 4986
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 4985 . . 3  |-  ( A 
C_  B  ->  `' A  C_  `' B )
2 cnvss 4985 . . 3  |-  ( B 
C_  A  ->  `' B  C_  `' A )
31, 2anim12i 574 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( `' A  C_  `' B  /\  `' B  C_  `' A ) )
4 eqss 3415 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
5 eqss 3415 . 2  |-  ( `' A  =  `' B  <->  ( `' A  C_  `' B  /\  `' B  C_  `' A
) )
63, 4, 53imtr4i 274 1  |-  ( A  =  B  ->  `' A  =  `' B
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    = wceq 1448    C_ wss 3372   `'ccnv 4811
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-in 3379  df-ss 3386  df-br 4375  df-opab 4434  df-cnv 4820
This theorem is referenced by:  cnveqi  4987  cnveqd  4988  rneq  5038  cnveqb  5270  predeq123  5360  f1eq1  5757  f1o00  5830  foeqcnvco  6184  funcnvuni  6734  tposfn2  6982  ereq1  7357  infeq3  7983  1arith  14882  vdwmc  14939  vdwnnlem1  14956  ramub2  14982  rami  14983  isps  16459  istsr  16474  isdir  16489  isrim0  17962  psrbag  18599  psrbaglefi  18607  iscn  20262  ishmeo  20785  symgtgp  21127  ustincl  21233  ustdiag  21234  ustinvel  21235  ustexhalf  21236  ustexsym  21241  ust0  21245  isi1f  22644  itg1val  22653  fta1lem  23272  fta1  23273  vieta1lem2  23276  vieta1  23277  sqff1o  24121  istrl  25279  isspth  25311  0spth  25313  nlfnval  27546  padct  28315  indf1ofs  28854  ismbfm  29080  issibf  29172  sitgfval  29180  eulerpartlemelr  29196  eulerpartleme  29202  eulerpartlemo  29204  eulerpartlemt0  29208  eulerpartlemt  29210  eulerpartgbij  29211  eulerpartlemr  29213  eulerpartlemgs2  29219  eulerpartlemn  29220  eulerpart  29221  iscvm  29988  elmpst  30180  wlimeq12  30508  lkrval  32656  ltrncnvnid  33694  cdlemkuu  34464  pw2f1o2val  35896  pwfi2f1o  35956  clcnvlem  36232  f1ssf1  39115  isTrl  39787  issPth  39810  upgrwlkdvspth  39823  uhgr1wlkspthlem1  39837  0spth-av  39894  isrngisom  40221
  Copyright terms: Public domain W3C validator