Theorem cnveq 5874

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ⊆ wss 3949  ^◡ccnv 5676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-br 5150  df-opab 5212  df-cnv 5685

This theorem is referenced by:  cnveqi  5875  cnveqd  5876  rneq  5936  cnveqb  6196  predeq123  6302  f1eq1  6783  f1ssf1  6866  f1o00  6869  foeqcnvco  7298  funcnvuni  7922  tposfn2  8233  ereq1  8710  cnvfi  9180  infeq3  9475  1arith  16860  vdwmc  16911  vdwnnlem1  16928  ramub2  16947  rami  16948  isps  18521  istsr  18536  isdir  18551  isrim0OLD  20259  isrim0  20261  psrbag  21470  psrbaglefi  21485  psrbaglefiOLD  21486  iscn  22739  ishmeo  23263  symgtgp  23610  ustincl  23712  ustdiag  23713  ustinvel  23714  ustexhalf  23715  ustexsym  23720  ust0  23724  isi1f  25191  itg1val  25200  fta1lem  25820  fta1  25821  vieta1lem2  25824  vieta1  25825  sqff1o  26686  istrl  28953  isspth  28981  upgrwlkdvspth  28996  uhgrwkspthlem1  29010  0spth  29379  nlfnval  31134  padct  31944  tocyc01  32277  cycpmconjslem2  32314  indf1ofs  33024  ismbfm  33249  issibf  33332  sitgfval  33340  eulerpartlemelr  33356  eulerpartleme  33362  eulerpartlemo  33364  eulerpartlemt0  33368  eulerpartlemt  33370  eulerpartgbij  33371  eulerpartlemr  33373  eulerpartlemgs2  33379  eulerpartlemn  33380  eulerpart  33381  funen1cnv  34091  iscvm  34250  elmpst  34527  elsymrels2  37423  elsymrels4  37425  symreleq  37428  elrefsymrels2  37439  eleqvrels2  37462  eldisjs  37592  lkrval  37958  ltrncnvnid  38998  cdlemkuu  39766  pw2f1o2val  41778  pwfi2f1o  41838  clcnvlem  42374  rfovcnvf1od  42755  fsovrfovd  42760  issmflem  45443  isrngisom  46694