Theorem cnveq 5781

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 5780	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵)
2		cnvss 5780	. . 3 ⊢ (𝐵 ⊆ 𝐴 → ◡𝐵 ⊆ ◡𝐴)
3	1, 2	anim12i 613	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴))
4		eqss 3941	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3941	. 2 ⊢ (◡𝐴 = ◡𝐵 ↔ (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴))
6	3, 4, 5	3imtr4i 292	1 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1542   ⊆ wss 3892  ^◡ccnv 5589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-in 3899  df-ss 3909  df-br 5080  df-opab 5142  df-cnv 5598

This theorem is referenced by:  cnveqi  5782  cnveqd  5783  rneq  5844  cnveqb  6098  predeq123  6202  f1eq1  6663  f1ssf1  6745  f1o00  6748  foeqcnvco  7168  funcnvuni  7772  tposfn2  8055  ereq1  8488  cnvfi  8945  infeq3  9217  1arith  16626  vdwmc  16677  vdwnnlem1  16694  ramub2  16713  rami  16714  isps  18284  istsr  18299  isdir  18314  isrim0  19965  psrbag  21118  psrbaglefi  21133  psrbaglefiOLD  21134  iscn  22384  ishmeo  22908  symgtgp  23255  ustincl  23357  ustdiag  23358  ustinvel  23359  ustexhalf  23360  ustexsym  23365  ust0  23369  isi1f  24836  itg1val  24845  fta1lem  25465  fta1  25466  vieta1lem2  25469  vieta1  25470  sqff1o  26329  istrl  28061  isspth  28088  upgrwlkdvspth  28103  uhgrwkspthlem1  28117  0spth  28486  nlfnval  30239  padct  31050  tocyc01  31381  cycpmconjslem2  31418  indf1ofs  31990  ismbfm  32215  issibf  32296  sitgfval  32304  eulerpartlemelr  32320  eulerpartleme  32326  eulerpartlemo  32328  eulerpartlemt0  32332  eulerpartlemt  32334  eulerpartgbij  32335  eulerpartlemr  32337  eulerpartlemgs2  32343  eulerpartlemn  32344  eulerpart  32345  funen1cnv  33056  iscvm  33217  elmpst  33494  elsymrels2  36663  elsymrels4  36665  symreleq  36668  elrefsymrels2  36679  eleqvrels2  36701  eldisjs  36829  lkrval  37098  ltrncnvnid  38137  cdlemkuu  38905  pw2f1o2val  40858  pwfi2f1o  40918  clcnvlem  41201  rfovcnvf1od  41582  fsovrfovd  41587  issmflem  44231  isrngisom  45423