Theorem cnveq 5005

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 5004	. . 3 |- ( A C_ B -> `' A C_ `' B )
2		cnvss 5004	. . 3 |- ( B C_ A -> `' B C_ `' A )
3	1, 2	anim12i 550	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( `' A C_ `' B /\ `' B C_ `' A ) )
4		eqss 3323	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
5		eqss 3323	. 2 |- ( `' A = `' B <-> ( `' A C_ `' B /\ `' B C_ `' A ) )
6	3, 4, 5	3imtr4i 258	1 |- ( A = B -> `' A = `' B )

Syntax hints:   -> wi 4   /\ wa 359   = wceq 1649   C_ wss 3280   `'ccnv 4836

This theorem is referenced by:  cnveqi  5006  cnveqd  5007  rneq  5054  cnveqb  5285  funcnvuni  5477  f1eq1  5593  f1o00  5669  foeqcnvco  5986  tposfn2  6460  ereq1  6871  wemapso2  7477  cantnfs  7577  oemapso  7594  mapfien  7609  1arith  13250  vdwmc  13301  vdwnnlem1  13318  ramub2  13337  rami  13338  isps  14589  istsr  14604  isdir  14632  dprdw  15523  psrbag  16386  psrbaglefi  16392  mplelbas  16449  mplsubglem  16453  mpllsslem  16454  ltbwe  16488  iscn  17253  ishmeo  17744  symgtgp  18084  ustincl  18190  ustdiag  18191  ustinvel  18192  ustexhalf  18193  ustexsym  18198  ust0  18202  isi1f  19519  itg1val  19528  mdegval  19939  fta1lem  20177  fta1  20178  vieta1lem2  20181  vieta1  20182  sqff1o  20918  istrl  21490  isspth  21522  0spth  21524  nlfnval  23337  indf1ofs  24376  ismbfm  24555  issibf  24601  sitgfval  24608  iscvm  24899  predeq1  25383  pw2f1o2val  27000  frlmelbas  27092  frlmssuvc1  27114  frlmssuvc2  27115  frlmsslsp  27116  ellspd  27122  pwfi2f1o  27128  islindf4  27176  lkrval  29571  ltrncnvnid  30609  cdlemkuu  31377

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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-in 3287  df-ss 3294  df-br 4173  df-opab 4227  df-cnv 4845