Theorem cnveq 4996

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 4995	. . 3 |- ( A C_ B -> `' A C_ `' B )
2		cnvss 4995	. . 3 |- ( B C_ A -> `' B C_ `' A )
3	1, 2	anim12i 564	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( `' A C_ `' B /\ `' B C_ `' A ) )
4		eqss 3456	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
5		eqss 3456	. 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 367   = wceq 1405   C_ wss 3413   `'ccnv 4821

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-in 3420  df-ss 3427  df-br 4395  df-opab 4453  df-cnv 4830

This theorem is referenced by:  cnveqi  4997  cnveqd  4998  rneq  5048  cnveqb  5278  predeq123  5367  f1eq1  5758  f1o00  5830  foeqcnvco  6185  funcnvuni  6736  tposfn2  6979  ereq1  7354  wemapso2OLD  8010  cantnfsOLD  8146  mapfienOLD  8169  1arith  14652  vdwmc  14703  vdwnnlem1  14720  ramub2  14739  rami  14740  isps  16154  istsr  16169  isdir  16184  dprdwOLD  17368  isrim0  17690  psrbag  18331  psrbaglefi  18341  psrbaglefiOLD  18342  mplelbasOLD  18407  mplsubglemOLD  18413  mpllsslemOLD  18414  iscn  20027  ishmeo  20550  symgtgp  20890  ustincl  21000  ustdiag  21001  ustinvel  21002  ustexhalf  21003  ustexsym  21008  ust0  21012  isi1f  22371  itg1val  22380  mdegvalOLD  22753  fta1lem  22993  fta1  22994  vieta1lem2  22997  vieta1  22998  sqff1o  23835  istrl  24943  isspth  24975  0spth  24977  nlfnval  27199  padct  27978  indf1ofs  28459  ismbfm  28686  issibf  28767  sitgfval  28775  eulerpartlemelr  28788  eulerpartleme  28794  eulerpartlemo  28796  eulerpartlemt0  28800  eulerpartlemt  28802  eulerpartgbij  28803  eulerpartlemr  28805  eulerpartlemgs2  28811  eulerpartlemn  28812  eulerpart  28813  iscvm  29543  elmpst  29735  wlimeq12  30062  lkrval  32086  ltrncnvnid  33124  cdlemkuu  33894  pw2f1o2val  35323  pwfi2f1o  35386  pwfi2f1oOLD  35387  isrngisom  38194