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

Step	Hyp	Ref	Expression
1		cnvss 4985	. . 3 |- ( A C_ B -> `' A C_ `' B )
2		cnvss 4985	. . 3 |- ( B C_ A -> `' B C_ `' A )
3	1, 2	anim12i 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 ) )
6	3, 4, 5	3imtr4i 274	1 |- ( A = B -> `' A = `' B )

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