Theorem cnveq 5826

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

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

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 3907  df-br 5087  df-opab 5149  df-cnv 5636

This theorem is referenced by:  cnveqi  5827  cnveqd  5828  rneq  5889  cnveqb  6158  predeq123  6264  f1eq1  6729  f1ssf1  6810  f1o00  6813  foeqcnvco  7252  funcnvuni  7880  tposfn2  8195  ereq1  8648  cnvfi  9107  infeq3  9391  1arith  16895  vdwmc  16946  vdwnnlem1  16963  ramub2  16982  rami  16983  isps  18531  istsr  18546  isdir  18561  isrngim  20422  isrim0  20459  psrbag  21913  psrbaglefi  21922  iscn  23216  ishmeo  23740  symgtgp  24087  ustincl  24189  ustdiag  24190  ustinvel  24191  ustexhalf  24192  ustexsym  24197  ust0  24201  isi1f  25657  itg1val  25666  fta1lem  26290  fta1  26291  vieta1lem2  26294  vieta1  26295  sqff1o  27165  istrl  29784  isspth  29811  upgrwlkdvspth  29828  uhgrwkspthlem1  29842  0spth  30217  nlfnval  31973  padct  32812  indf1ofs  32947  tocyc01  33200  cycpmconjslem2  33237  ismbfm  34417  issibf  34499  sitgfval  34507  eulerpartlemelr  34523  eulerpartleme  34529  eulerpartlemo  34531  eulerpartlemt0  34535  eulerpartlemt  34537  eulerpartgbij  34538  eulerpartlemr  34540  eulerpartlemgs2  34546  eulerpartlemn  34547  eulerpart  34548  funen1cnv  35253  iscvm  35463  elmpst  35740  elsymrels2  38980  elsymrels4  38982  symreleq  38985  elrefsymrels2  38996  eleqvrels2  39019  eldisjs  39162  lkrval  39556  ltrncnvnid  40595  cdlemkuu  41363  pw2f1o2val  43493  pwfi2f1o  43550  clcnvlem  44076  rfovcnvf1od  44457  fsovrfovd  44462  issmflem  47181