Theorem cnveq 5543

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 5542	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵)
2		cnvss 5542	. . 3 ⊢ (𝐵 ⊆ 𝐴 → ◡𝐵 ⊆ ◡𝐴)
3	1, 2	anim12i 606	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴))
4		eqss 3836	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3836	. 2 ⊢ (◡𝐴 = ◡𝐵 ↔ (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴))
6	3, 4, 5	3imtr4i 284	1 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)

Syntax hints:   → wi 4   ∧ wa 386   = wceq 1601   ⊆ wss 3792  ^◡ccnv 5356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-in 3799  df-ss 3806  df-br 4889  df-opab 4951  df-cnv 5365

This theorem is referenced by:  cnveqi  5544  cnveqd  5545  rneq  5598  cnveqb  5845  predeq123  5936  f1eq1  6348  f1ssf1  6424  f1o00  6427  foeqcnvco  6829  funcnvuni  7400  tposfn2  7658  ereq1  8035  infeq3  8676  1arith  16039  vdwmc  16090  vdwnnlem1  16107  ramub2  16126  rami  16127  isps  17592  istsr  17607  isdir  17622  isrim0  19116  psrbag  19765  psrbaglefi  19773  iscn  21451  ishmeo  21975  symgtgp  22317  ustincl  22423  ustdiag  22424  ustinvel  22425  ustexhalf  22426  ustexsym  22431  ust0  22435  isi1f  23882  itg1val  23891  fta1lem  24503  fta1  24504  vieta1lem2  24507  vieta1  24508  sqff1o  25364  istrl  27051  isspth  27080  upgrwlkdvspth  27095  uhgrwkspthlem1  27109  0spth  27533  nlfnval  29316  padct  30067  indf1ofs  30690  ismbfm  30916  issibf  30997  sitgfval  31005  eulerpartlemelr  31021  eulerpartleme  31027  eulerpartlemo  31029  eulerpartlemt0  31033  eulerpartlemt  31035  eulerpartgbij  31036  eulerpartlemr  31038  eulerpartlemgs2  31044  eulerpartlemn  31045  eulerpart  31046  iscvm  31844  elmpst  32036  elsymrels2  34932  elsymrels4  34934  symreleq  34937  elrefsymrels2  34948  eleqvrels2  34969  lkrval  35247  ltrncnvnid  36286  cdlemkuu  37054  pw2f1o2val  38575  pwfi2f1o  38635  clcnvlem  38897  rfovcnvf1od  39264  fsovrfovd  39269  issmflem  41873  isrngisom  42921