Theorem cnveq 5812

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ⊆ wss 3897  ^◡ccnv 5613

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ss 3914  df-br 5090  df-opab 5152  df-cnv 5622

This theorem is referenced by:  cnveqi  5813  cnveqd  5814  rneq  5875  cnveqb  6143  predeq123  6249  f1eq1  6714  f1ssf1  6795  f1o00  6798  foeqcnvco  7234  funcnvuni  7862  tposfn2  8178  ereq1  8629  cnvfi  9085  infeq3  9365  1arith  16839  vdwmc  16890  vdwnnlem1  16907  ramub2  16926  rami  16927  isps  18474  istsr  18489  isdir  18504  isrngim  20363  isrim0  20400  psrbag  21854  psrbaglefi  21863  iscn  23150  ishmeo  23674  symgtgp  24021  ustincl  24123  ustdiag  24124  ustinvel  24125  ustexhalf  24126  ustexsym  24131  ust0  24135  isi1f  25602  itg1val  25611  fta1lem  26242  fta1  26243  vieta1lem2  26246  vieta1  26247  sqff1o  27119  istrl  29673  isspth  29700  upgrwlkdvspth  29717  uhgrwkspthlem1  29731  0spth  30106  nlfnval  31861  padct  32701  indf1ofs  32847  tocyc01  33087  cycpmconjslem2  33124  ismbfm  34264  issibf  34346  sitgfval  34354  eulerpartlemelr  34370  eulerpartleme  34376  eulerpartlemo  34378  eulerpartlemt0  34382  eulerpartlemt  34384  eulerpartgbij  34385  eulerpartlemr  34387  eulerpartlemgs2  34393  eulerpartlemn  34394  eulerpart  34395  funen1cnv  35100  iscvm  35303  elmpst  35580  elsymrels2  38648  elsymrels4  38650  symreleq  38653  elrefsymrels2  38664  eleqvrels2  38687  eldisjs  38819  lkrval  39186  ltrncnvnid  40225  cdlemkuu  40993  pw2f1o2val  43131  pwfi2f1o  43188  clcnvlem  43715  rfovcnvf1od  44096  fsovrfovd  44101  issmflem  46824