Theorem cnveq 5510

Description: Equality theorem for converse. (Contributed by NM, 13-Aug-1995.)

Assertion

Ref	Expression
cnveq	⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)

Proof of Theorem cnveq

Step	Hyp	Ref	Expression
1		cnvss 5509	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵)
2		cnvss 5509	. . 3 ⊢ (𝐵 ⊆ 𝐴 → ◡𝐵 ⊆ ◡𝐴)
3	1, 2	anim12i 602	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴))
4		eqss 3824	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3824	. 2 ⊢ (◡𝐴 = ◡𝐵 ↔ (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴))
6	3, 4, 5	3imtr4i 283	1 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1637   ⊆ wss 3780  ^◡ccnv 5323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-in 3787  df-ss 3794  df-br 4856  df-opab 4918  df-cnv 5332

This theorem is referenced by:  cnveqi  5511  cnveqd  5512  rneq  5565  cnveqb  5814  predeq123  5907  f1eq1  6320  f1ssf1  6393  f1o00  6396  foeqcnvco  6788  funcnvuni  7358  tposfn2  7618  ereq1  7995  infeq3  8634  1arith  15867  vdwmc  15918  vdwnnlem1  15935  ramub2  15954  rami  15955  isps  17426  istsr  17441  isdir  17456  isrim0  18946  psrbag  19592  psrbaglefi  19600  iscn  21273  ishmeo  21796  symgtgp  22138  ustincl  22244  ustdiag  22245  ustinvel  22246  ustexhalf  22247  ustexsym  22252  ust0  22256  isi1f  23677  itg1val  23686  fta1lem  24298  fta1  24299  vieta1lem2  24302  vieta1  24303  sqff1o  25144  istrl  26843  isspth  26870  upgrwlkdvspth  26885  uhgrwkspthlem1  26899  0spth  27321  nlfnval  29090  padct  29846  indf1ofs  30435  ismbfm  30661  issibf  30742  sitgfval  30750  eulerpartlemelr  30766  eulerpartleme  30772  eulerpartlemo  30774  eulerpartlemt0  30778  eulerpartlemt  30780  eulerpartgbij  30781  eulerpartlemr  30783  eulerpartlemgs2  30789  eulerpartlemn  30790  eulerpart  30791  iscvm  31585  elmpst  31777  elsymrels2  34630  elsymrels4  34632  symreleq  34635  elrefsymrels2  34646  lkrval  34886  ltrncnvnid  35925  cdlemkuu  36693  pw2f1o2val  38124  pwfi2f1o  38184  clcnvlem  38447  rfovcnvf1od  38815  fsovrfovd  38820  issmflem  41435  isrngisom  42481