Theorem cnveq 5857

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 5856	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵)
2		cnvss 5856	. . 3 ⊢ (𝐵 ⊆ 𝐴 → ◡𝐵 ⊆ ◡𝐴)
3	1, 2	anim12i 625	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴))
4		eqss 3949	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3949	. 2 ⊢ (◡𝐴 = ◡𝐵 ↔ (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴))
6	3, 4, 5	3imtr4i 295	1 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ⊆ wss 3902  ^◡ccnv 5658

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ss 3919  df-br 5108  df-opab 5172  df-cnv 5667

This theorem is used by:  cnveqi  5858  cnveqd  5859  rneq  5924  cnveqb  6194  predeq123  6304  f1eq1  6770  f1ssf1  6854  f1o00  6857  foeqcnvco  7304  funcnvuni  7932  tposfn2  8249  ereq1  8707  funen1cnv  9038  cnvfi  9173  infeq3  9454  1arith  17023  vdwmc  17074  vdwnnlem1  17091  ramub2  17110  rami  17111  isps  18660  istsr  18675  isdir  18690  isrngim  20587  isrim0  20625  psrbag  22133  psrbaglefi  22142  iscn  23461  ishmeo  23986  symgtgp  24333  ustincl  24435  ustdiag  24436  ustinvel  24437  ustexhalf  24438  ustexsym  24443  ust0  24447  isi1f  25903  itg1val  25912  fta1lem  26538  fta1  26539  vieta1lem2  26542  vieta1  26543  sqff1o  27416  istrl  30144  isspth  30172  upgrwlkdvspth  30190  uhgrwkspthlem1  30204  0spth  30582  nlfnval  32348  padct  33176  indf1ofs  33299  tocyc01  33545  cycpmconjslem2  33582  ismbfm  34749  issibf  34831  sitgfval  34839  eulerpartlemelr  34855  eulerpartleme  34861  eulerpartlemo  34863  eulerpartlemt0  34867  eulerpartlemt  34869  eulerpartgbij  34870  eulerpartlemr  34872  eulerpartlemgs2  34878  eulerpartlemn  34879  eulerpart  34880  iscvm  35825  elmpst  36102  elsymrels2  39372  elsymrels4  39374  symreleq  39377  elrefsymrels2  39388  eleqvrels2  39411  eldisjs  39554  lkrval  39948  ltrncnvnid  40987  cdlemkuu  41755  pw2f1o2val  43867  pwfi2f1o  43924  clcnvlem  44450  rfovcnvf1od  44831  fsovrfovd  44836  issmflem  47542