Theorem cnveq 5821

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ⊆ wss 3900  ^◡ccnv 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-ss 3917  df-br 5098  df-opab 5160  df-cnv 5631

This theorem is referenced by:  cnveqi  5822  cnveqd  5823  rneq  5884  cnveqb  6153  predeq123  6259  f1eq1  6724  f1ssf1  6805  f1o00  6808  foeqcnvco  7246  funcnvuni  7874  tposfn2  8190  ereq1  8643  cnvfi  9102  infeq3  9386  1arith  16857  vdwmc  16908  vdwnnlem1  16925  ramub2  16944  rami  16945  isps  18493  istsr  18508  isdir  18523  isrngim  20383  isrim0  20420  psrbag  21875  psrbaglefi  21884  iscn  23181  ishmeo  23705  symgtgp  24052  ustincl  24154  ustdiag  24155  ustinvel  24156  ustexhalf  24157  ustexsym  24162  ust0  24166  isi1f  25633  itg1val  25642  fta1lem  26273  fta1  26274  vieta1lem2  26277  vieta1  26278  sqff1o  27150  istrl  29749  isspth  29776  upgrwlkdvspth  29793  uhgrwkspthlem1  29807  0spth  30182  nlfnval  31937  padct  32776  indf1ofs  32927  tocyc01  33179  cycpmconjslem2  33216  ismbfm  34387  issibf  34469  sitgfval  34477  eulerpartlemelr  34493  eulerpartleme  34499  eulerpartlemo  34501  eulerpartlemt0  34505  eulerpartlemt  34507  eulerpartgbij  34508  eulerpartlemr  34510  eulerpartlemgs2  34516  eulerpartlemn  34517  eulerpart  34518  funen1cnv  35223  iscvm  35432  elmpst  35709  elsymrels2  38807  elsymrels4  38809  symreleq  38812  elrefsymrels2  38823  eleqvrels2  38846  eldisjs  38989  lkrval  39383  ltrncnvnid  40422  cdlemkuu  41190  pw2f1o2val  43318  pwfi2f1o  43375  clcnvlem  43901  rfovcnvf1od  44282  fsovrfovd  44287  issmflem  47008