Theorem cnveq 5847

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1562   ⊆ wss 3906  ^◡ccnv 5648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ss 3923  df-br 5103  df-opab 5165  df-cnv 5657

This theorem is referenced by:  cnveqi  5848  cnveqd  5849  rneq  5914  cnveqb  6185  predeq123  6291  f1eq1  6757  f1ssf1  6841  f1o00  6844  foeqcnvco  7286  funcnvuni  7915  tposfn2  8230  ereq1  8688  cnvfi  9146  infeq3  9429  1arith  16965  vdwmc  17016  vdwnnlem1  17033  ramub2  17052  rami  17053  isps  18602  istsr  18617  isdir  18632  isrngim  20496  isrim0  20533  psrbag  21971  psrbaglefi  21980  iscn  23297  ishmeo  23821  symgtgp  24168  ustincl  24270  ustdiag  24271  ustinvel  24272  ustexhalf  24273  ustexsym  24278  ust0  24282  isi1f  25738  itg1val  25747  fta1lem  26373  fta1  26374  vieta1lem2  26377  vieta1  26378  sqff1o  27248  istrl  29897  isspth  29924  upgrwlkdvspth  29941  uhgrwkspthlem1  29955  0spth  30330  nlfnval  32086  padct  32922  indf1ofs  33046  tocyc01  33300  cycpmconjslem2  33337  ismbfm  34550  issibf  34632  sitgfval  34640  eulerpartlemelr  34656  eulerpartleme  34662  eulerpartlemo  34664  eulerpartlemt0  34668  eulerpartlemt  34670  eulerpartgbij  34671  eulerpartlemr  34673  eulerpartlemgs2  34679  eulerpartlemn  34680  eulerpart  34681  funen1cnv  35384  iscvm  35614  elmpst  35891  elsymrels2  39141  elsymrels4  39143  symreleq  39146  elrefsymrels2  39157  eleqvrels2  39180  eldisjs  39323  lkrval  39717  ltrncnvnid  40756  cdlemkuu  41524  pw2f1o2val  43621  pwfi2f1o  43678  clcnvlem  44204  rfovcnvf1od  44585  fsovrfovd  44590  issmflem  47306