Theorem cnveq 5850

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ⊆ wss 3895  ^◡ccnv 5649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3896  df-br 5103  df-opab 5167  df-cnv 5658

This theorem is used by:  cnveqi  5851  cnveqd  5852  rneq  5917  predeq123  6305  f1eq1  6773  f1ssf1  6857  f1o00  6860  foeqcnvco  7308  funcnvuni  7944  tposfn2  8265  ereq1  8725  funen1cnv  9056  cnvfi  9191  infeq3  9473  1arith  17105  vdwmc  17156  vdwnnlem1  17173  ramub2  17192  rami  17193  isps  18742  istsr  18757  isdir  18772  isrngim  20675  isrim0  20713  psrbag  22225  psrbaglefi  22234  iscn  23553  ishmeo  24078  symgtgp  24425  ustincl  24527  ustdiag  24528  ustinvel  24529  ustexhalf  24530  ustexsym  24535  ust0  24539  isi1f  25995  itg1val  26004  fta1lem  26628  fta1  26629  vieta1lem2  26634  vieta1  26635  sqff1o  27509  istrl  30279  isspth  30307  upgrwlkdvspth  30325  uhgrwkspthlem1  30339  0spth  30717  nlfnval  32483  padct  33310  indf1ofs  33433  tocyc01  33679  cycpmconjslem2  33716  ismbfm  34884  issibf  34965  sitgfval  34973  eulerpartlemelr  34989  eulerpartleme  34995  eulerpartlemo  34997  eulerpartlemt0  35001  eulerpartlemt  35003  eulerpartgbij  35004  eulerpartlemr  35006  eulerpartlemgs2  35012  eulerpartlemn  35013  eulerpart  35014  iscvm  36024  elmpst  36301  elsymrels2  39570  elsymrels4  39572  symreleq  39575  elrefsymrels2  39586  eleqvrels2  39609  eldisjs  39752  lkrval  40146  ltrncnvnid  41185  cdlemkuu  41953  pw2f1o2val  44046  pwfi2f1o  44098  clcnvlem  44623  rfovcnvf1od  45004  fsovrfovd  45009  issmflem  47737