Theorem cnveq 5027

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 5026	. . 3 |- ( A C_ B -> `' A C_ `' B )
2		cnvss 5026	. . 3 |- ( B C_ A -> `' B C_ `' A )
3	1, 2	anim12i 568	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( `' A C_ `' B /\ `' B C_ `' A ) )
4		eqss 3479	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
5		eqss 3479	. 2 |- ( `' A = `' B <-> ( `' A C_ `' B /\ `' B C_ `' A ) )
6	3, 4, 5	3imtr4i 269	1 |- ( A = B -> `' A = `' B )

Syntax hints:   -> wi 4   /\ wa 370   = wceq 1437   C_ wss 3436   `'ccnv 4852

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-in 3443  df-ss 3450  df-br 4424  df-opab 4483  df-cnv 4861

This theorem is referenced by:  cnveqi  5028  cnveqd  5029  rneq  5079  cnveqb  5310  predeq123  5400  f1eq1  5791  f1o00  5863  foeqcnvco  6213  funcnvuni  6760  tposfn2  7006  ereq1  7381  infeq3  8005  1arith  14870  vdwmc  14927  vdwnnlem1  14944  ramub2  14970  rami  14971  isps  16447  istsr  16462  isdir  16477  isrim0  17950  psrbag  18587  psrbaglefi  18595  iscn  20249  ishmeo  20772  symgtgp  21114  ustincl  21220  ustdiag  21221  ustinvel  21222  ustexhalf  21223  ustexsym  21228  ust0  21232  isi1f  22630  itg1val  22639  fta1lem  23258  fta1  23259  vieta1lem2  23262  vieta1  23263  sqff1o  24107  istrl  25265  isspth  25297  0spth  25299  nlfnval  27532  padct  28313  indf1ofs  28855  ismbfm  29082  issibf  29174  sitgfval  29182  eulerpartlemelr  29198  eulerpartleme  29204  eulerpartlemo  29206  eulerpartlemt0  29210  eulerpartlemt  29212  eulerpartgbij  29213  eulerpartlemr  29215  eulerpartlemgs2  29221  eulerpartlemn  29222  eulerpart  29223  iscvm  29990  elmpst  30182  wlimeq12  30509  lkrval  32623  ltrncnvnid  33661  cdlemkuu  34431  pw2f1o2val  35864  pwfi2f1o  35924  clcnvlem  36200  f1ssf1  38884  isrngisom  39515