Theorem cnveq 5786

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

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

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 2103  ax-9 2111  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1540  df-ex 1778  df-sb 2063  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3436  df-in 3896  df-ss 3906  df-br 5078  df-opab 5140  df-cnv 5599

This theorem is referenced by:  cnveqi  5787  cnveqd  5788  rneq  5848  cnveqb  6103  predeq123  6207  f1eq1  6683  f1ssf1  6766  f1o00  6769  foeqcnvco  7192  funcnvuni  7798  tposfn2  8084  ereq1  8525  cnvfi  8988  infeq3  9267  1arith  16656  vdwmc  16707  vdwnnlem1  16724  ramub2  16743  rami  16744  isps  18314  istsr  18329  isdir  18344  isrim0  19995  psrbag  21148  psrbaglefi  21163  psrbaglefiOLD  21164  iscn  22414  ishmeo  22938  symgtgp  23285  ustincl  23387  ustdiag  23388  ustinvel  23389  ustexhalf  23390  ustexsym  23395  ust0  23399  isi1f  24866  itg1val  24875  fta1lem  25495  fta1  25496  vieta1lem2  25499  vieta1  25500  sqff1o  26359  istrl  28092  isspth  28120  upgrwlkdvspth  28135  uhgrwkspthlem1  28149  0spth  28518  nlfnval  30271  padct  31082  tocyc01  31413  cycpmconjslem2  31450  indf1ofs  32022  ismbfm  32247  issibf  32328  sitgfval  32336  eulerpartlemelr  32352  eulerpartleme  32358  eulerpartlemo  32360  eulerpartlemt0  32364  eulerpartlemt  32366  eulerpartgbij  32367  eulerpartlemr  32369  eulerpartlemgs2  32375  eulerpartlemn  32376  eulerpart  32377  funen1cnv  33088  iscvm  33249  elmpst  33526  elsymrels2  36693  elsymrels4  36695  symreleq  36698  elrefsymrels2  36709  eleqvrels2  36731  eldisjs  36859  lkrval  37128  ltrncnvnid  38167  cdlemkuu  38935  pw2f1o2val  40885  pwfi2f1o  40945  clcnvlem  41255  rfovcnvf1od  41636  fsovrfovd  41641  issmflem  44301  isrngisom  45494