Theorem cnveq 5296

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 5294	. . 3 |- ( A C_ B -> `' A C_ `' B )
2		cnvss 5294	. . 3 |- ( B C_ A -> `' B C_ `' A )
3	1, 2	anim12i 590	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( `' A C_ `' B /\ `' B C_ `' A ) )
4		eqss 3618	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
5		eqss 3618	. 2 |- ( `' A = `' B <-> ( `' A C_ `' B /\ `' B C_ `' A ) )
6	3, 4, 5	3imtr4i 281	1 |- ( A = B -> `' A = `' B )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   C_ wss 3574   `'ccnv 5113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-in 3581  df-ss 3588  df-br 4654  df-opab 4713  df-cnv 5122

This theorem is referenced by:  cnveqi  5297  cnveqd  5298  rneq  5351  cnveqb  5590  predeq123  5681  f1eq1  6096  f1ssf1  6168  f1o00  6171  foeqcnvco  6555  funcnvuni  7119  tposfn2  7374  ereq1  7749  infeq3  8386  1arith  15631  vdwmc  15682  vdwnnlem1  15699  ramub2  15718  rami  15719  isps  17202  istsr  17217  isdir  17232  isrim0  18723  psrbag  19364  psrbaglefi  19372  iscn  21039  ishmeo  21562  symgtgp  21905  ustincl  22011  ustdiag  22012  ustinvel  22013  ustexhalf  22014  ustexsym  22019  ust0  22023  isi1f  23441  itg1val  23450  fta1lem  24062  fta1  24063  vieta1lem2  24066  vieta1  24067  sqff1o  24908  istrl  26593  isspth  26620  upgrwlkdvspth  26635  uhgrwkspthlem1  26649  0spth  26987  nlfnval  28740  padct  29497  indf1ofs  30088  ismbfm  30314  issibf  30395  sitgfval  30403  eulerpartlemelr  30419  eulerpartleme  30425  eulerpartlemo  30427  eulerpartlemt0  30431  eulerpartlemt  30433  eulerpartgbij  30434  eulerpartlemr  30436  eulerpartlemgs2  30442  eulerpartlemn  30443  eulerpart  30444  iscvm  31241  elmpst  31433  lkrval  34375  ltrncnvnid  35413  cdlemkuu  36183  pw2f1o2val  37606  pwfi2f1o  37666  clcnvlem  37930  rfovcnvf1od  38298  fsovrfovd  38303  issmflem  40936  isrngisom  41896