Theorem cnveq 5818

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 5817	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵)
2		cnvss 5817	. . 3 ⊢ (𝐵 ⊆ 𝐴 → ◡𝐵 ⊆ ◡𝐴)
3	1, 2	anim12i 620	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴))
4		eqss 3932	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3932	. 2 ⊢ (◡𝐴 = ◡𝐵 ↔ (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴))
6	3, 4, 5	3imtr4i 294	1 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1548   ⊆ wss 3885  ^◡ccnv 5620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ss 3902  df-br 5076  df-opab 5138  df-cnv 5629

This theorem is referenced by:  cnveqi  5819  cnveqd  5820  rneq  5885  cnveqb  6151  predeq123  6257  f1eq1  6722  f1ssf1  6803  f1o00  6806  foeqcnvco  7248  funcnvuni  7876  tposfn2  8192  ereq1  8645  cnvfi  9104  infeq3  9388  1arith  16893  vdwmc  16944  vdwnnlem1  16961  ramub2  16980  rami  16981  isps  18529  istsr  18544  isdir  18559  isrngim  20420  isrim0  20457  psrbag  21896  psrbaglefi  21905  iscn  23222  ishmeo  23746  symgtgp  24093  ustincl  24195  ustdiag  24196  ustinvel  24197  ustexhalf  24198  ustexsym  24203  ust0  24207  isi1f  25663  itg1val  25672  fta1lem  26295  fta1  26296  vieta1lem2  26299  vieta1  26300  sqff1o  27167  istrl  29785  isspth  29812  upgrwlkdvspth  29829  uhgrwkspthlem1  29843  0spth  30218  nlfnval  31974  padct  32814  indf1ofs  32949  tocyc01  33203  cycpmconjslem2  33240  ismbfm  34447  issibf  34529  sitgfval  34537  eulerpartlemelr  34553  eulerpartleme  34559  eulerpartlemo  34561  eulerpartlemt0  34565  eulerpartlemt  34567  eulerpartgbij  34568  eulerpartlemr  34570  eulerpartlemgs2  34576  eulerpartlemn  34577  eulerpart  34578  funen1cnv  35284  iscvm  35502  elmpst  35779  elsymrels2  39019  elsymrels4  39021  symreleq  39024  elrefsymrels2  39035  eleqvrels2  39058  eldisjs  39201  lkrval  39595  ltrncnvnid  40634  cdlemkuu  41402  pw2f1o2val  43499  pwfi2f1o  43556  clcnvlem  44082  rfovcnvf1od  44463  fsovrfovd  44468  issmflem  47184