Theorem cnveq 5739

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 5738	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵)
2		cnvss 5738	. . 3 ⊢ (𝐵 ⊆ 𝐴 → ◡𝐵 ⊆ ◡𝐴)
3	1, 2	anim12i 614	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴))
4		eqss 3982	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3982	. 2 ⊢ (◡𝐴 = ◡𝐵 ↔ (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴))
6	3, 4, 5	3imtr4i 294	1 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1533   ⊆ wss 3936  ^◡ccnv 5549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-in 3943  df-ss 3952  df-br 5060  df-opab 5122  df-cnv 5558

This theorem is referenced by:  cnveqi  5740  cnveqd  5741  rneq  5801  cnveqb  6048  predeq123  6144  f1eq1  6565  f1ssf1  6641  f1o00  6644  foeqcnvco  7050  funcnvuni  7630  tposfn2  7908  ereq1  8290  infeq3  8938  1arith  16257  vdwmc  16308  vdwnnlem1  16325  ramub2  16344  rami  16345  isps  17806  istsr  17821  isdir  17836  isrim0  19469  psrbag  20138  psrbaglefi  20146  iscn  21837  ishmeo  22361  symgtgp  22708  ustincl  22810  ustdiag  22811  ustinvel  22812  ustexhalf  22813  ustexsym  22818  ust0  22822  isi1f  24269  itg1val  24278  fta1lem  24890  fta1  24891  vieta1lem2  24894  vieta1  24895  sqff1o  25753  istrl  27472  isspth  27499  upgrwlkdvspth  27514  uhgrwkspthlem1  27528  0spth  27899  nlfnval  29652  padct  30449  tocyc01  30755  cycpmconjslem2  30792  indf1ofs  31280  ismbfm  31505  issibf  31586  sitgfval  31594  eulerpartlemelr  31610  eulerpartleme  31616  eulerpartlemo  31618  eulerpartlemt0  31622  eulerpartlemt  31624  eulerpartgbij  31625  eulerpartlemr  31627  eulerpartlemgs2  31633  eulerpartlemn  31634  eulerpart  31635  funen1cnv  32352  iscvm  32501  elmpst  32778  elsymrels2  35783  elsymrels4  35785  symreleq  35788  elrefsymrels2  35799  eleqvrels2  35821  eldisjs  35949  lkrval  36218  ltrncnvnid  37257  cdlemkuu  38025  pw2f1o2val  39629  pwfi2f1o  39689  clcnvlem  39976  rfovcnvf1od  40343  fsovrfovd  40348  issmflem  42997  isrngisom  44160