Theorem cnveq 5834

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ⊆ wss 3913  ^◡ccnv 5637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930  df-br 5111  df-opab 5173  df-cnv 5646

This theorem is referenced by:  cnveqi  5835  cnveqd  5836  rneq  5896  cnveqb  6153  predeq123  6259  f1eq1  6738  f1ssf1  6821  f1o00  6824  foeqcnvco  7251  funcnvuni  7873  tposfn2  8184  ereq1  8662  cnvfi  9131  infeq3  9425  1arith  16810  vdwmc  16861  vdwnnlem1  16878  ramub2  16897  rami  16898  isps  18471  istsr  18486  isdir  18501  isrim0OLD  20170  isrim0  20172  psrbag  21356  psrbaglefi  21371  psrbaglefiOLD  21372  iscn  22623  ishmeo  23147  symgtgp  23494  ustincl  23596  ustdiag  23597  ustinvel  23598  ustexhalf  23599  ustexsym  23604  ust0  23608  isi1f  25075  itg1val  25084  fta1lem  25704  fta1  25705  vieta1lem2  25708  vieta1  25709  sqff1o  26568  istrl  28707  isspth  28735  upgrwlkdvspth  28750  uhgrwkspthlem1  28764  0spth  29133  nlfnval  30886  padct  31704  tocyc01  32037  cycpmconjslem2  32074  indf1ofs  32714  ismbfm  32939  issibf  33022  sitgfval  33030  eulerpartlemelr  33046  eulerpartleme  33052  eulerpartlemo  33054  eulerpartlemt0  33058  eulerpartlemt  33060  eulerpartgbij  33061  eulerpartlemr  33063  eulerpartlemgs2  33069  eulerpartlemn  33070  eulerpart  33071  funen1cnv  33781  iscvm  33940  elmpst  34217  elsymrels2  37088  elsymrels4  37090  symreleq  37093  elrefsymrels2  37104  eleqvrels2  37127  eldisjs  37257  lkrval  37623  ltrncnvnid  38663  cdlemkuu  39431  pw2f1o2val  41421  pwfi2f1o  41481  clcnvlem  42017  rfovcnvf1od  42398  fsovrfovd  42403  issmflem  45088  isrngisom  46314