Theorem cnveq 5832

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ⊆ wss 3903  ^◡ccnv 5633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3920  df-br 5101  df-opab 5163  df-cnv 5642

This theorem is referenced by:  cnveqi  5833  cnveqd  5834  rneq  5895  cnveqb  6164  predeq123  6270  f1eq1  6735  f1ssf1  6816  f1o00  6819  foeqcnvco  7258  funcnvuni  7886  tposfn2  8202  ereq1  8655  cnvfi  9114  infeq3  9398  1arith  16869  vdwmc  16920  vdwnnlem1  16937  ramub2  16956  rami  16957  isps  18505  istsr  18520  isdir  18535  isrngim  20398  isrim0  20435  psrbag  21890  psrbaglefi  21899  iscn  23196  ishmeo  23720  symgtgp  24067  ustincl  24169  ustdiag  24170  ustinvel  24171  ustexhalf  24172  ustexsym  24177  ust0  24181  isi1f  25648  itg1val  25657  fta1lem  26288  fta1  26289  vieta1lem2  26292  vieta1  26293  sqff1o  27165  istrl  29786  isspth  29813  upgrwlkdvspth  29830  uhgrwkspthlem1  29844  0spth  30219  nlfnval  31975  padct  32814  indf1ofs  32965  tocyc01  33218  cycpmconjslem2  33255  ismbfm  34435  issibf  34517  sitgfval  34525  eulerpartlemelr  34541  eulerpartleme  34547  eulerpartlemo  34549  eulerpartlemt0  34553  eulerpartlemt  34555  eulerpartgbij  34556  eulerpartlemr  34558  eulerpartlemgs2  34564  eulerpartlemn  34565  eulerpart  34566  funen1cnv  35271  iscvm  35481  elmpst  35758  elsymrels2  38917  elsymrels4  38919  symreleq  38922  elrefsymrels2  38933  eleqvrels2  38956  eldisjs  39099  lkrval  39493  ltrncnvnid  40532  cdlemkuu  41300  pw2f1o2val  43425  pwfi2f1o  43482  clcnvlem  44008  rfovcnvf1od  44389  fsovrfovd  44394  issmflem  47114