Theorem cnveq 5771

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 5770	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵)
2		cnvss 5770	. . 3 ⊢ (𝐵 ⊆ 𝐴 → ◡𝐵 ⊆ ◡𝐴)
3	1, 2	anim12i 612	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴))
4		eqss 3932	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3932	. 2 ⊢ (◡𝐴 = ◡𝐵 ↔ (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴))
6	3, 4, 5	3imtr4i 291	1 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ⊆ wss 3883  ^◡ccnv 5579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-br 5071  df-opab 5133  df-cnv 5588

This theorem is referenced by:  cnveqi  5772  cnveqd  5773  rneq  5834  cnveqb  6088  predeq123  6192  f1eq1  6649  f1ssf1  6731  f1o00  6734  foeqcnvco  7152  funcnvuni  7752  tposfn2  8035  ereq1  8463  cnvfi  8924  infeq3  9169  1arith  16556  vdwmc  16607  vdwnnlem1  16624  ramub2  16643  rami  16644  isps  18201  istsr  18216  isdir  18231  isrim0  19882  psrbag  21030  psrbaglefi  21045  psrbaglefiOLD  21046  iscn  22294  ishmeo  22818  symgtgp  23165  ustincl  23267  ustdiag  23268  ustinvel  23269  ustexhalf  23270  ustexsym  23275  ust0  23279  isi1f  24743  itg1val  24752  fta1lem  25372  fta1  25373  vieta1lem2  25376  vieta1  25377  sqff1o  26236  istrl  27966  isspth  27993  upgrwlkdvspth  28008  uhgrwkspthlem1  28022  0spth  28391  nlfnval  30144  padct  30956  tocyc01  31287  cycpmconjslem2  31324  indf1ofs  31894  ismbfm  32119  issibf  32200  sitgfval  32208  eulerpartlemelr  32224  eulerpartleme  32230  eulerpartlemo  32232  eulerpartlemt0  32236  eulerpartlemt  32238  eulerpartgbij  32239  eulerpartlemr  32241  eulerpartlemgs2  32247  eulerpartlemn  32248  eulerpart  32249  funen1cnv  32960  iscvm  33121  elmpst  33398  elsymrels2  36594  elsymrels4  36596  symreleq  36599  elrefsymrels2  36610  eleqvrels2  36632  eldisjs  36760  lkrval  37029  ltrncnvnid  38068  cdlemkuu  38836  pw2f1o2val  40777  pwfi2f1o  40837  clcnvlem  41120  rfovcnvf1od  41501  fsovrfovd  41506  issmflem  44150  isrngisom  45342