Theorem cnveq 5823

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3919  df-br 5100  df-opab 5162  df-cnv 5633

This theorem is referenced by:  cnveqi  5824  cnveqd  5825  rneq  5886  cnveqb  6155  predeq123  6261  f1eq1  6726  f1ssf1  6807  f1o00  6810  foeqcnvco  7249  funcnvuni  7877  tposfn2  8193  ereq1  8646  cnvfi  9105  infeq3  9389  1arith  16860  vdwmc  16911  vdwnnlem1  16928  ramub2  16947  rami  16948  isps  18496  istsr  18511  isdir  18526  isrngim  20386  isrim0  20423  psrbag  21878  psrbaglefi  21887  iscn  23184  ishmeo  23708  symgtgp  24055  ustincl  24157  ustdiag  24158  ustinvel  24159  ustexhalf  24160  ustexsym  24165  ust0  24169  isi1f  25636  itg1val  25645  fta1lem  26276  fta1  26277  vieta1lem2  26280  vieta1  26281  sqff1o  27153  istrl  29773  isspth  29800  upgrwlkdvspth  29817  uhgrwkspthlem1  29831  0spth  30206  nlfnval  31961  padct  32800  indf1ofs  32951  tocyc01  33204  cycpmconjslem2  33241  ismbfm  34421  issibf  34503  sitgfval  34511  eulerpartlemelr  34527  eulerpartleme  34533  eulerpartlemo  34535  eulerpartlemt0  34539  eulerpartlemt  34541  eulerpartgbij  34542  eulerpartlemr  34544  eulerpartlemgs2  34550  eulerpartlemn  34551  eulerpart  34552  funen1cnv  35257  iscvm  35466  elmpst  35743  elsymrels2  38851  elsymrels4  38853  symreleq  38856  elrefsymrels2  38867  eleqvrels2  38890  eldisjs  39033  lkrval  39427  ltrncnvnid  40466  cdlemkuu  41234  pw2f1o2val  43359  pwfi2f1o  43416  clcnvlem  43942  rfovcnvf1od  44323  fsovrfovd  44328  issmflem  47048