Theorem cnveq 5837

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

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

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 3931  df-br 5108  df-opab 5170  df-cnv 5646

This theorem is referenced by:  cnveqi  5838  cnveqd  5839  rneq  5900  cnveqb  6169  predeq123  6275  f1eq1  6751  f1ssf1  6832  f1o00  6835  foeqcnvco  7275  funcnvuni  7908  tposfn2  8227  ereq1  8678  cnvfi  9140  infeq3  9432  1arith  16898  vdwmc  16949  vdwnnlem1  16966  ramub2  16985  rami  16986  isps  18527  istsr  18542  isdir  18557  isrngim  20354  isrim0OLD  20390  isrim0  20392  psrbag  21826  psrbaglefi  21835  iscn  23122  ishmeo  23646  symgtgp  23993  ustincl  24095  ustdiag  24096  ustinvel  24097  ustexhalf  24098  ustexsym  24103  ust0  24107  isi1f  25575  itg1val  25584  fta1lem  26215  fta1  26216  vieta1lem2  26219  vieta1  26220  sqff1o  27092  istrl  29624  isspth  29652  upgrwlkdvspth  29669  uhgrwkspthlem1  29683  0spth  30055  nlfnval  31810  padct  32643  indf1ofs  32789  tocyc01  33075  cycpmconjslem2  33112  ismbfm  34241  issibf  34324  sitgfval  34332  eulerpartlemelr  34348  eulerpartleme  34354  eulerpartlemo  34356  eulerpartlemt0  34360  eulerpartlemt  34362  eulerpartgbij  34363  eulerpartlemr  34365  eulerpartlemgs2  34371  eulerpartlemn  34372  eulerpart  34373  funen1cnv  35078  iscvm  35246  elmpst  35523  elsymrels2  38544  elsymrels4  38546  symreleq  38549  elrefsymrels2  38560  eleqvrels2  38583  eldisjs  38714  lkrval  39081  ltrncnvnid  40121  cdlemkuu  40889  pw2f1o2val  43028  pwfi2f1o  43085  clcnvlem  43612  rfovcnvf1od  43993  fsovrfovd  43998  issmflem  46725