Theorem cnveq 5863

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1568   ⊆ wss 3913  ^◡ccnv 5664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-ext 2742

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-sb 2099  df-clab 2749  df-cleq 2762  df-clel 2845  df-ss 3930  df-br 5115  df-opab 5179  df-cnv 5673

This theorem is referenced by:  cnveqi  5864  cnveqd  5865  rneq  5930  cnveqb  6199  predeq123  6307  f1eq1  6773  f1ssf1  6857  f1o00  6860  foeqcnvco  7302  funcnvuni  7932  tposfn2  8247  ereq1  8705  cnvfi  9163  infeq3  9444  1arith  16990  vdwmc  17041  vdwnnlem1  17058  ramub2  17077  rami  17078  isps  18627  istsr  18642  isdir  18657  isrngim  20530  isrim0  20567  psrbag  22050  psrbaglefi  22059  iscn  23375  ishmeo  23899  symgtgp  24246  ustincl  24348  ustdiag  24349  ustinvel  24350  ustexhalf  24351  ustexsym  24356  ust0  24360  isi1f  25816  itg1val  25825  fta1lem  26451  fta1  26452  vieta1lem2  26455  vieta1  26456  sqff1o  27326  istrl  30014  isspth  30041  upgrwlkdvspth  30058  uhgrwkspthlem1  30072  0spth  30447  nlfnval  32203  padct  33033  indf1ofs  33156  tocyc01  33408  cycpmconjslem2  33445  ismbfm  34611  issibf  34693  sitgfval  34701  eulerpartlemelr  34717  eulerpartleme  34723  eulerpartlemo  34725  eulerpartlemt0  34729  eulerpartlemt  34731  eulerpartgbij  34732  eulerpartlemr  34734  eulerpartlemgs2  34740  eulerpartlemn  34741  eulerpart  34742  funen1cnv  35445  iscvm  35709  elmpst  35986  elsymrels2  39236  elsymrels4  39238  symreleq  39241  elrefsymrels2  39252  eleqvrels2  39275  eldisjs  39418  lkrval  39812  ltrncnvnid  40851  cdlemkuu  41619  pw2f1o2val  43718  pwfi2f1o  43775  clcnvlem  44301  rfovcnvf1od  44682  fsovrfovd  44687  issmflem  47393