Theorem cnveq 5858

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ⊆ wss 3931  ^◡ccnv 5658

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ss 3948  df-br 5125  df-opab 5187  df-cnv 5667

This theorem is referenced by:  cnveqi  5859  cnveqd  5860  rneq  5921  cnveqb  6190  predeq123  6296  f1eq1  6774  f1ssf1  6855  f1o00  6858  foeqcnvco  7298  funcnvuni  7933  tposfn2  8252  ereq1  8731  cnvfi  9195  infeq3  9498  1arith  16952  vdwmc  17003  vdwnnlem1  17020  ramub2  17039  rami  17040  isps  18583  istsr  18598  isdir  18613  isrngim  20410  isrim0OLD  20446  isrim0  20448  psrbag  21882  psrbaglefi  21891  iscn  23178  ishmeo  23702  symgtgp  24049  ustincl  24151  ustdiag  24152  ustinvel  24153  ustexhalf  24154  ustexsym  24159  ust0  24163  isi1f  25632  itg1val  25641  fta1lem  26272  fta1  26273  vieta1lem2  26276  vieta1  26277  sqff1o  27149  istrl  29681  isspth  29709  upgrwlkdvspth  29726  uhgrwkspthlem1  29740  0spth  30112  nlfnval  31867  padct  32702  indf1ofs  32848  tocyc01  33134  cycpmconjslem2  33171  ismbfm  34287  issibf  34370  sitgfval  34378  eulerpartlemelr  34394  eulerpartleme  34400  eulerpartlemo  34402  eulerpartlemt0  34406  eulerpartlemt  34408  eulerpartgbij  34409  eulerpartlemr  34411  eulerpartlemgs2  34417  eulerpartlemn  34418  eulerpart  34419  funen1cnv  35124  iscvm  35286  elmpst  35563  elsymrels2  38576  elsymrels4  38578  symreleq  38581  elrefsymrels2  38592  eleqvrels2  38615  eldisjs  38745  lkrval  39111  ltrncnvnid  40151  cdlemkuu  40919  pw2f1o2val  43038  pwfi2f1o  43095  clcnvlem  43622  rfovcnvf1od  44003  fsovrfovd  44008  issmflem  46736