Theorem cnveq 5898

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ⊆ wss 3976  ^◡ccnv 5699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ss 3993  df-br 5167  df-opab 5229  df-cnv 5708

This theorem is referenced by:  cnveqi  5899  cnveqd  5900  rneq  5961  cnveqb  6227  predeq123  6333  f1eq1  6812  f1ssf1  6894  f1o00  6897  foeqcnvco  7336  funcnvuni  7972  tposfn2  8289  ereq1  8770  cnvfi  9243  infeq3  9549  1arith  16974  vdwmc  17025  vdwnnlem1  17042  ramub2  17061  rami  17062  isps  18638  istsr  18653  isdir  18668  isrngim  20471  isrim0OLD  20507  isrim0  20509  psrbag  21960  psrbaglefi  21969  iscn  23264  ishmeo  23788  symgtgp  24135  ustincl  24237  ustdiag  24238  ustinvel  24239  ustexhalf  24240  ustexsym  24245  ust0  24249  isi1f  25728  itg1val  25737  fta1lem  26367  fta1  26368  vieta1lem2  26371  vieta1  26372  sqff1o  27243  istrl  29732  isspth  29760  upgrwlkdvspth  29775  uhgrwkspthlem1  29789  0spth  30158  nlfnval  31913  padct  32733  tocyc01  33111  cycpmconjslem2  33148  indf1ofs  33990  ismbfm  34215  issibf  34298  sitgfval  34306  eulerpartlemelr  34322  eulerpartleme  34328  eulerpartlemo  34330  eulerpartlemt0  34334  eulerpartlemt  34336  eulerpartgbij  34337  eulerpartlemr  34339  eulerpartlemgs2  34345  eulerpartlemn  34346  eulerpart  34347  funen1cnv  35064  iscvm  35227  elmpst  35504  elsymrels2  38509  elsymrels4  38511  symreleq  38514  elrefsymrels2  38525  eleqvrels2  38548  eldisjs  38678  lkrval  39044  ltrncnvnid  40084  cdlemkuu  40852  pw2f1o2val  42996  pwfi2f1o  43053  clcnvlem  43585  rfovcnvf1od  43966  fsovrfovd  43971  issmflem  46648