Theorem cnveq 5848

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 5847	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵)
2		cnvss 5847	. . 3 ⊢ (𝐵 ⊆ 𝐴 → ◡𝐵 ⊆ ◡𝐴)
3	1, 2	anim12i 625	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴))
4		eqss 3946	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3946	. 2 ⊢ (◡𝐴 = ◡𝐵 ↔ (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴))
6	3, 4, 5	3imtr4i 295	1 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ⊆ wss 3899  ^◡ccnv 5647

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3916  df-br 5104  df-opab 5168  df-cnv 5656

This theorem is used by:  cnveqi  5849  cnveqd  5850  rneq  5915  cnveqb  6185  predeq123  6295  f1eq1  6762  f1ssf1  6846  f1o00  6849  foeqcnvco  7297  funcnvuni  7928  tposfn2  8244  ereq1  8704  funen1cnv  9035  cnvfi  9170  infeq3  9451  1arith  17052  vdwmc  17103  vdwnnlem1  17120  ramub2  17139  rami  17140  isps  18689  istsr  18704  isdir  18719  isrngim  20622  isrim0  20660  psrbag  22172  psrbaglefi  22181  iscn  23500  ishmeo  24025  symgtgp  24372  ustincl  24474  ustdiag  24475  ustinvel  24476  ustexhalf  24477  ustexsym  24482  ust0  24486  isi1f  25942  itg1val  25951  fta1lem  26577  fta1  26578  vieta1lem2  26583  vieta1  26584  sqff1o  27458  istrl  30198  isspth  30226  upgrwlkdvspth  30244  uhgrwkspthlem1  30258  0spth  30636  nlfnval  32402  padct  33229  indf1ofs  33352  tocyc01  33598  cycpmconjslem2  33635  ismbfm  34803  issibf  34885  sitgfval  34893  eulerpartlemelr  34909  eulerpartleme  34915  eulerpartlemo  34917  eulerpartlemt0  34921  eulerpartlemt  34923  eulerpartgbij  34924  eulerpartlemr  34926  eulerpartlemgs2  34932  eulerpartlemn  34933  eulerpart  34934  iscvm  35939  elmpst  36216  elsymrels2  39483  elsymrels4  39485  symreleq  39488  elrefsymrels2  39499  eleqvrels2  39522  eldisjs  39665  lkrval  40059  ltrncnvnid  41098  cdlemkuu  41866  pw2f1o2val  43978  pwfi2f1o  44035  clcnvlem  44561  rfovcnvf1od  44942  fsovrfovd  44947  issmflem  47653