Theorem cnveq 5827

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ⊆ wss 3911  ^◡ccnv 5630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3928  df-br 5103  df-opab 5165  df-cnv 5639

This theorem is referenced by:  cnveqi  5828  cnveqd  5829  rneq  5889  cnveqb  6157  predeq123  6263  f1eq1  6733  f1ssf1  6814  f1o00  6817  foeqcnvco  7257  funcnvuni  7888  tposfn2  8204  ereq1  8655  cnvfi  9117  infeq3  9408  1arith  16875  vdwmc  16926  vdwnnlem1  16943  ramub2  16962  rami  16963  isps  18510  istsr  18525  isdir  18540  isrngim  20366  isrim0OLD  20402  isrim0  20404  psrbag  21860  psrbaglefi  21869  iscn  23156  ishmeo  23680  symgtgp  24027  ustincl  24129  ustdiag  24130  ustinvel  24131  ustexhalf  24132  ustexsym  24137  ust0  24141  isi1f  25609  itg1val  25618  fta1lem  26249  fta1  26250  vieta1lem2  26253  vieta1  26254  sqff1o  27126  istrl  29676  isspth  29703  upgrwlkdvspth  29720  uhgrwkspthlem1  29734  0spth  30106  nlfnval  31861  padct  32694  indf1ofs  32840  tocyc01  33091  cycpmconjslem2  33128  ismbfm  34235  issibf  34318  sitgfval  34326  eulerpartlemelr  34342  eulerpartleme  34348  eulerpartlemo  34350  eulerpartlemt0  34354  eulerpartlemt  34356  eulerpartgbij  34357  eulerpartlemr  34359  eulerpartlemgs2  34365  eulerpartlemn  34366  eulerpart  34367  funen1cnv  35072  iscvm  35240  elmpst  35517  elsymrels2  38538  elsymrels4  38540  symreleq  38543  elrefsymrels2  38554  eleqvrels2  38577  eldisjs  38708  lkrval  39075  ltrncnvnid  40115  cdlemkuu  40883  pw2f1o2val  43022  pwfi2f1o  43079  clcnvlem  43606  rfovcnvf1od  43987  fsovrfovd  43992  issmflem  46719