Theorem cnveq 5883

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 5882	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵)
2		cnvss 5882	. . 3 ⊢ (𝐵 ⊆ 𝐴 → ◡𝐵 ⊆ ◡𝐴)
3	1, 2	anim12i 613	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴))
4		eqss 3998	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3998	. 2 ⊢ (◡𝐴 = ◡𝐵 ↔ (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴))
6	3, 4, 5	3imtr4i 292	1 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ⊆ wss 3950  ^◡ccnv 5683

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ss 3967  df-br 5143  df-opab 5205  df-cnv 5692

This theorem is referenced by:  cnveqi  5884  cnveqd  5885  rneq  5946  cnveqb  6215  predeq123  6321  f1eq1  6798  f1ssf1  6879  f1o00  6882  foeqcnvco  7321  funcnvuni  7955  tposfn2  8274  ereq1  8753  cnvfi  9217  infeq3  9521  1arith  16966  vdwmc  17017  vdwnnlem1  17034  ramub2  17053  rami  17054  isps  18614  istsr  18629  isdir  18644  isrngim  20446  isrim0OLD  20482  isrim0  20484  psrbag  21938  psrbaglefi  21947  iscn  23244  ishmeo  23768  symgtgp  24115  ustincl  24217  ustdiag  24218  ustinvel  24219  ustexhalf  24220  ustexsym  24225  ust0  24229  isi1f  25710  itg1val  25719  fta1lem  26350  fta1  26351  vieta1lem2  26354  vieta1  26355  sqff1o  27226  istrl  29715  isspth  29743  upgrwlkdvspth  29760  uhgrwkspthlem1  29774  0spth  30146  nlfnval  31901  padct  32732  indf1ofs  32852  tocyc01  33139  cycpmconjslem2  33176  ismbfm  34253  issibf  34336  sitgfval  34344  eulerpartlemelr  34360  eulerpartleme  34366  eulerpartlemo  34368  eulerpartlemt0  34372  eulerpartlemt  34374  eulerpartgbij  34375  eulerpartlemr  34377  eulerpartlemgs2  34383  eulerpartlemn  34384  eulerpart  34385  funen1cnv  35103  iscvm  35265  elmpst  35542  elsymrels2  38555  elsymrels4  38557  symreleq  38560  elrefsymrels2  38571  eleqvrels2  38594  eldisjs  38724  lkrval  39090  ltrncnvnid  40130  cdlemkuu  40898  pw2f1o2val  43056  pwfi2f1o  43113  clcnvlem  43641  rfovcnvf1od  44022  fsovrfovd  44027  issmflem  46747