Theorem cnveq 5817

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 5816	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵)
2		cnvss 5816	. . 3 ⊢ (𝐵 ⊆ 𝐴 → ◡𝐵 ⊆ ◡𝐴)
3	1, 2	anim12i 614	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴))
4		eqss 3932	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3932	. 2 ⊢ (◡𝐴 = ◡𝐵 ↔ (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴))
6	3, 4, 5	3imtr4i 292	1 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ⊆ wss 3885  ^◡ccnv 5619

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-ss 3902  df-br 5075  df-opab 5137  df-cnv 5628

This theorem is referenced by:  cnveqi  5818  cnveqd  5819  rneq  5880  cnveqb  6149  predeq123  6255  f1eq1  6720  f1ssf1  6801  f1o00  6804  foeqcnvco  7244  funcnvuni  7872  tposfn2  8187  ereq1  8640  cnvfi  9099  infeq3  9383  1arith  16887  vdwmc  16938  vdwnnlem1  16955  ramub2  16974  rami  16975  isps  18523  istsr  18538  isdir  18553  isrngim  20414  isrim0  20451  psrbag  21886  psrbaglefi  21895  iscn  23188  ishmeo  23712  symgtgp  24059  ustincl  24161  ustdiag  24162  ustinvel  24163  ustexhalf  24164  ustexsym  24169  ust0  24173  isi1f  25629  itg1val  25638  fta1lem  26261  fta1  26262  vieta1lem2  26265  vieta1  26266  sqff1o  27133  istrl  29751  isspth  29778  upgrwlkdvspth  29795  uhgrwkspthlem1  29809  0spth  30184  nlfnval  31940  padct  32779  indf1ofs  32914  tocyc01  33167  cycpmconjslem2  33204  ismbfm  34383  issibf  34465  sitgfval  34473  eulerpartlemelr  34489  eulerpartleme  34495  eulerpartlemo  34497  eulerpartlemt0  34501  eulerpartlemt  34503  eulerpartgbij  34504  eulerpartlemr  34506  eulerpartlemgs2  34512  eulerpartlemn  34513  eulerpart  34514  funen1cnv  35219  iscvm  35429  elmpst  35706  elsymrels2  38946  elsymrels4  38948  symreleq  38951  elrefsymrels2  38962  eleqvrels2  38985  eldisjs  39128  lkrval  39522  ltrncnvnid  40561  cdlemkuu  41329  pw2f1o2val  43455  pwfi2f1o  43512  clcnvlem  44038  rfovcnvf1od  44419  fsovrfovd  44424  issmflem  47143