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  29644  isspth  29671  upgrwlkdvspth  29688  uhgrwkspthlem1  29702  0spth  30074  nlfnval  31829  padct  32670  indf1ofs  32818  tocyc01  33069  cycpmconjslem2  33106  ismbfm  34234  issibf  34317  sitgfval  34325  eulerpartlemelr  34341  eulerpartleme  34347  eulerpartlemo  34349  eulerpartlemt0  34353  eulerpartlemt  34355  eulerpartgbij  34356  eulerpartlemr  34358  eulerpartlemgs2  34364  eulerpartlemn  34365  eulerpart  34366  funen1cnv  35071  iscvm  35252  elmpst  35529  elsymrels2  38550  elsymrels4  38552  symreleq  38555  elrefsymrels2  38566  eleqvrels2  38589  eldisjs  38720  lkrval  39087  ltrncnvnid  40126  cdlemkuu  40894  pw2f1o2val  43032  pwfi2f1o  43089  clcnvlem  43616  rfovcnvf1od  43997  fsovrfovd  44002  issmflem  46728