Theorem cnveq 5176

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 5175	. . 3 |- ( A C_ B -> `' A C_ `' B )
2		cnvss 5175	. . 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 3519	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
5		eqss 3519	. 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 1379   C_ wss 3476   `'ccnv 4998

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-in 3483  df-ss 3490  df-br 4448  df-opab 4506  df-cnv 5007

This theorem is referenced by:  cnveqi  5177  cnveqd  5178  rneq  5228  cnveqb  5462  f1eq1  5776  f1o00  5848  foeqcnvco  6191  funcnvuni  6737  tposfn2  6977  ereq1  7318  wemapso2OLD  7977  cantnfsOLD  8115  mapfienOLD  8138  1arith  14304  vdwmc  14355  vdwnnlem1  14372  ramub2  14391  rami  14392  isps  15689  istsr  15704  isdir  15719  dprdwOLD  16852  isrim0  17173  psrbag  17812  psrbaglefi  17822  psrbaglefiOLD  17823  mplelbasOLD  17888  mplsubglemOLD  17894  mpllsslemOLD  17895  frlmelbasOLD  18584  frlmssuvc1OLD  18622  frlmssuvc2OLD  18623  frlmsslspOLD  18625  ellspdOLD  18632  iscn  19530  ishmeo  20023  symgtgp  20363  ustincl  20473  ustdiag  20474  ustinvel  20475  ustexhalf  20476  ustexsym  20481  ust0  20485  isi1f  21844  itg1val  21853  mdegvalOLD  22226  fta1lem  22465  fta1  22466  vieta1lem2  22469  vieta1  22470  sqff1o  23212  istrl  24243  isspth  24275  0spth  24277  nlfnval  26504  indf1ofs  27707  ismbfm  27891  issibf  27943  sitgfval  27951  eulerpartlemelr  27964  eulerpartleme  27970  eulerpartlemo  27972  eulerpartlemt0  27976  eulerpartlemt  27978  eulerpartgbij  27979  eulerpartlemr  27981  eulerpartlemgs2  27987  eulerpartlemn  27988  eulerpart  27989  iscvm  28372  predeq123  28850  wlimeq12  28980  pw2f1o2val  30613  pwfi2f1o  30676  lkrval  33903  ltrncnvnid  34941  cdlemkuu  35709