Theorem cnveq 5218

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 5216	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵)
2		cnvss 5216	. . 3 ⊢ (𝐵 ⊆ 𝐴 → ◡𝐵 ⊆ ◡𝐴)
3	1, 2	anim12i 588	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴))
4		eqss 3583	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3583	. 2 ⊢ (◡𝐴 = ◡𝐵 ↔ (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴))
6	3, 4, 5	3imtr4i 280	1 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ⊆ wss 3540  ^◡ccnv 5037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-in 3547  df-ss 3554  df-br 4584  df-opab 4644  df-cnv 5046

This theorem is referenced by:  cnveqi  5219  cnveqd  5220  rneq  5272  cnveqb  5508  predeq123  5598  f1eq1  6009  f1o00  6083  foeqcnvco  6455  funcnvuni  7012  tposfn2  7261  ereq1  7636  infeq3  8269  1arith  15469  vdwmc  15520  vdwnnlem1  15537  ramub2  15556  rami  15557  isps  17025  istsr  17040  isdir  17055  isrim0  18546  psrbag  19185  psrbaglefi  19193  iscn  20849  ishmeo  21372  symgtgp  21715  ustincl  21821  ustdiag  21822  ustinvel  21823  ustexhalf  21824  ustexsym  21829  ust0  21833  isi1f  23247  itg1val  23256  fta1lem  23866  fta1  23867  vieta1lem2  23870  vieta1  23871  sqff1o  24708  istrl  26067  isspth  26099  0spth  26101  nlfnval  28124  padct  28885  indf1ofs  29415  ismbfm  29641  issibf  29722  sitgfval  29730  eulerpartlemelr  29746  eulerpartleme  29752  eulerpartlemo  29754  eulerpartlemt0  29758  eulerpartlemt  29760  eulerpartgbij  29761  eulerpartlemr  29763  eulerpartlemgs2  29769  eulerpartlemn  29770  eulerpart  29771  iscvm  30495  elmpst  30687  lkrval  33393  ltrncnvnid  34431  cdlemkuu  35201  pw2f1o2val  36624  pwfi2f1o  36684  clcnvlem  36949  rfovcnvf1od  37318  fsovrfovd  37323  issmflem  39613  f1ssf1  40328  isTrl  40904  issPth  40930  upgrwlkdvspth  40945  uhgr1wlkspthlem1  40959  0spth-av  41294  isrngisom  41686