Theorem cnveq 5816

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

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

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 3920  df-br 5093  df-opab 5155  df-cnv 5627

This theorem is referenced by:  cnveqi  5817  cnveqd  5818  rneq  5878  cnveqb  6145  predeq123  6250  f1eq1  6715  f1ssf1  6796  f1o00  6799  foeqcnvco  7237  funcnvuni  7865  tposfn2  8181  ereq1  8632  cnvfi  9090  infeq3  9371  1arith  16839  vdwmc  16890  vdwnnlem1  16907  ramub2  16926  rami  16927  isps  18474  istsr  18489  isdir  18504  isrngim  20330  isrim0OLD  20366  isrim0  20368  psrbag  21824  psrbaglefi  21833  iscn  23120  ishmeo  23644  symgtgp  23991  ustincl  24093  ustdiag  24094  ustinvel  24095  ustexhalf  24096  ustexsym  24101  ust0  24105  isi1f  25573  itg1val  25582  fta1lem  26213  fta1  26214  vieta1lem2  26217  vieta1  26218  sqff1o  27090  istrl  29640  isspth  29667  upgrwlkdvspth  29684  uhgrwkspthlem1  29698  0spth  30070  nlfnval  31825  padct  32662  indf1ofs  32809  tocyc01  33060  cycpmconjslem2  33097  ismbfm  34218  issibf  34301  sitgfval  34309  eulerpartlemelr  34325  eulerpartleme  34331  eulerpartlemo  34333  eulerpartlemt0  34337  eulerpartlemt  34339  eulerpartgbij  34340  eulerpartlemr  34342  eulerpartlemgs2  34348  eulerpartlemn  34349  eulerpart  34350  funen1cnv  35055  iscvm  35236  elmpst  35513  elsymrels2  38534  elsymrels4  38536  symreleq  38539  elrefsymrels2  38550  eleqvrels2  38573  eldisjs  38704  lkrval  39071  ltrncnvnid  40110  cdlemkuu  40878  pw2f1o2val  43016  pwfi2f1o  43073  clcnvlem  43600  rfovcnvf1od  43981  fsovrfovd  43986  issmflem  46712