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  28984  isspth  29012  upgrwlkdvspth  29027  uhgrwkspthlem1  29041  0spth  29410  nlfnval  31165  padct  31975  tocyc01  32308  cycpmconjslem2  32345  indf1ofs  33055  ismbfm  33280  issibf  33363  sitgfval  33371  eulerpartlemelr  33387  eulerpartleme  33393  eulerpartlemo  33395  eulerpartlemt0  33399  eulerpartlemt  33401  eulerpartgbij  33402  eulerpartlemr  33404  eulerpartlemgs2  33410  eulerpartlemn  33411  eulerpart  33412  funen1cnv  34122  iscvm  34281  elmpst  34558  elsymrels2  37471  elsymrels4  37473  symreleq  37476  elrefsymrels2  37487  eleqvrels2  37510  eldisjs  37640  lkrval  38006  ltrncnvnid  39046  cdlemkuu  39814  pw2f1o2val  41826  pwfi2f1o  41886  clcnvlem  42422  rfovcnvf1od  42803  fsovrfovd  42808  issmflem  45491  isrngisom  46742