Theorem cnveq 5858

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   = wceq 1569   ⊆ wss 3904  ^◡ccnv 5659

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ss 3921  df-br 5109  df-opab 5173  df-cnv 5668

This theorem is used by:  cnveqi  5859  cnveqd  5860  rneq  5925  cnveqb  6194  predeq123  6303  f1eq1  6769  f1ssf1  6853  f1o00  6856  foeqcnvco  7298  funcnvuni  7927  tposfn2  8242  ereq1  8700  cnvfi  9158  infeq3  9439  1arith  16993  vdwmc  17044  vdwnnlem1  17061  ramub2  17080  rami  17081  isps  18630  istsr  18645  isdir  18660  isrngim  20534  isrim0  20572  psrbag  22078  psrbaglefi  22087  iscn  23403  ishmeo  23927  symgtgp  24274  ustincl  24376  ustdiag  24377  ustinvel  24378  ustexhalf  24379  ustexsym  24384  ust0  24388  isi1f  25844  itg1val  25853  fta1lem  26479  fta1  26480  vieta1lem2  26483  vieta1  26484  sqff1o  27357  istrl  30055  isspth  30082  upgrwlkdvspth  30099  uhgrwkspthlem1  30113  0spth  30488  nlfnval  32244  padct  33074  indf1ofs  33197  tocyc01  33447  cycpmconjslem2  33484  ismbfm  34650  issibf  34732  sitgfval  34740  eulerpartlemelr  34756  eulerpartleme  34762  eulerpartlemo  34764  eulerpartlemt0  34768  eulerpartlemt  34770  eulerpartgbij  34771  eulerpartlemr  34773  eulerpartlemgs2  34779  eulerpartlemn  34780  eulerpart  34781  funen1cnv  35486  iscvm  35759  elmpst  36036  elsymrels2  39314  elsymrels4  39316  symreleq  39319  elrefsymrels2  39330  eleqvrels2  39353  eldisjs  39496  lkrval  39890  ltrncnvnid  40929  cdlemkuu  41697  pw2f1o2val  43794  pwfi2f1o  43851  clcnvlem  44377  rfovcnvf1od  44758  fsovrfovd  44763  issmflem  47469