Theorem cnveq 5018

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 5017	. . 3 |- ( A C_ B -> `' A C_ `' B )
2		cnvss 5017	. . 3 |- ( B C_ A -> `' B C_ `' A )
3	1, 2	anim12i 566	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( `' A C_ `' B /\ `' B C_ `' A ) )
4		eqss 3376	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
5		eqss 3376	. 2 |- ( `' A = `' B <-> ( `' A C_ `' B /\ `' B C_ `' A ) )
6	3, 4, 5	3imtr4i 266	1 |- ( A = B -> `' A = `' B )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1369   C_ wss 3333   `'ccnv 4844

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-in 3340  df-ss 3347  df-br 4298  df-opab 4356  df-cnv 4853

This theorem is referenced by:  cnveqi  5019  cnveqd  5020  rneq  5070  cnveqb  5298  f1eq1  5606  f1o00  5678  foeqcnvco  6003  funcnvuni  6535  tposfn2  6772  ereq1  7113  wemapso2OLD  7771  cantnfsOLD  7909  mapfienOLD  7932  1arith  13993  vdwmc  14044  vdwnnlem1  14061  ramub2  14080  rami  14081  isps  15377  istsr  15392  isdir  15407  dprdwOLD  16505  isrim0  16818  psrbag  17436  psrbaglefi  17446  psrbaglefiOLD  17447  mplelbasOLD  17511  mplsubglemOLD  17517  mpllsslemOLD  17518  frlmelbasOLD  18188  frlmssuvc1OLD  18226  frlmssuvc2OLD  18227  frlmsslspOLD  18229  ellspdOLD  18236  iscn  18844  ishmeo  19337  symgtgp  19677  ustincl  19787  ustdiag  19788  ustinvel  19789  ustexhalf  19790  ustexsym  19795  ust0  19799  isi1f  21157  itg1val  21166  mdegvalOLD  21539  fta1lem  21778  fta1  21779  vieta1lem2  21782  vieta1  21783  sqff1o  22525  istrl  23441  isspth  23473  0spth  23475  nlfnval  25290  indf1ofs  26487  ismbfm  26672  issibf  26724  sitgfval  26732  eulerpartlemelr  26745  eulerpartleme  26751  eulerpartlemo  26753  eulerpartlemt0  26757  eulerpartlemt  26759  eulerpartgbij  26760  eulerpartlemr  26762  eulerpartlemgs2  26768  eulerpartlemn  26769  eulerpart  26770  iscvm  27153  predeq123  27631  wlimeq12  27761  pw2f1o2val  29393  pwfi2f1o  29456  lkrval  32738  ltrncnvnid  33776  cdlemkuu  34544