Theorem cnveq 5876

Description: Equality theorem for converse relation. (Contributed by NM, 13-Aug-1995.)

Assertion

Ref	Expression
cnveq	⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)

Proof of Theorem cnveq

Step	Hyp	Ref	Expression
1		cnvss 5875	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵)
2		cnvss 5875	. . 3 ⊢ (𝐵 ⊆ 𝐴 → ◡𝐵 ⊆ ◡𝐴)
3	1, 2	anim12i 611	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴))
4		eqss 3992	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3992	. 2 ⊢ (◡𝐴 = ◡𝐵 ↔ (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴))
6	3, 4, 5	3imtr4i 291	1 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1533   ⊆ wss 3944  ^◡ccnv 5677

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ss 3961  df-br 5150  df-opab 5212  df-cnv 5686

This theorem is referenced by:  cnveqi  5877  cnveqd  5878  rneq  5938  cnveqb  6202  predeq123  6308  f1eq1  6788  f1ssf1  6870  f1o00  6873  foeqcnvco  7309  funcnvuni  7940  tposfn2  8254  ereq1  8732  cnvfi  9205  infeq3  9505  1arith  16899  vdwmc  16950  vdwnnlem1  16967  ramub2  16986  rami  16987  isps  18563  istsr  18578  isdir  18593  isrngim  20396  isrim0OLD  20432  isrim0  20434  psrbag  21867  psrbaglefi  21882  psrbaglefiOLD  21883  iscn  23183  ishmeo  23707  symgtgp  24054  ustincl  24156  ustdiag  24157  ustinvel  24158  ustexhalf  24159  ustexsym  24164  ust0  24168  isi1f  25647  itg1val  25656  fta1lem  26287  fta1  26288  vieta1lem2  26291  vieta1  26292  sqff1o  27159  istrl  29582  isspth  29610  upgrwlkdvspth  29625  uhgrwkspthlem1  29639  0spth  30008  nlfnval  31763  padct  32583  tocyc01  32931  cycpmconjslem2  32968  indf1ofs  33776  ismbfm  34001  issibf  34084  sitgfval  34092  eulerpartlemelr  34108  eulerpartleme  34114  eulerpartlemo  34116  eulerpartlemt0  34120  eulerpartlemt  34122  eulerpartgbij  34123  eulerpartlemr  34125  eulerpartlemgs2  34131  eulerpartlemn  34132  eulerpart  34133  funen1cnv  34842  iscvm  35000  elmpst  35277  elsymrels2  38155  elsymrels4  38157  symreleq  38160  elrefsymrels2  38171  eleqvrels2  38194  eldisjs  38324  lkrval  38690  ltrncnvnid  39730  cdlemkuu  40498  pw2f1o2val  42602  pwfi2f1o  42662  clcnvlem  43195  rfovcnvf1od  43576  fsovrfovd  43581  issmflem  46253