Theorem cnveq 5708

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 5707	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵)
2		cnvss 5707	. . 3 ⊢ (𝐵 ⊆ 𝐴 → ◡𝐵 ⊆ ◡𝐴)
3	1, 2	anim12i 615	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴))
4		eqss 3930	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3930	. 2 ⊢ (◡𝐴 = ◡𝐵 ↔ (◡𝐴 ⊆ ◡𝐵 ∧ ◡𝐵 ⊆ ◡𝐴))
6	3, 4, 5	3imtr4i 295	1 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ⊆ wss 3881  ^◡ccnv 5518

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-br 5031  df-opab 5093  df-cnv 5527

This theorem is referenced by:  cnveqi  5709  cnveqd  5710  rneq  5770  cnveqb  6020  predeq123  6117  f1eq1  6544  f1ssf1  6621  f1o00  6624  foeqcnvco  7034  funcnvuni  7618  tposfn2  7897  ereq1  8279  infeq3  8928  1arith  16253  vdwmc  16304  vdwnnlem1  16321  ramub2  16340  rami  16341  isps  17804  istsr  17819  isdir  17834  isrim0  19471  psrbag  20602  psrbaglefi  20610  iscn  21840  ishmeo  22364  symgtgp  22711  ustincl  22813  ustdiag  22814  ustinvel  22815  ustexhalf  22816  ustexsym  22821  ust0  22825  isi1f  24278  itg1val  24287  fta1lem  24903  fta1  24904  vieta1lem2  24907  vieta1  24908  sqff1o  25767  istrl  27486  isspth  27513  upgrwlkdvspth  27528  uhgrwkspthlem1  27542  0spth  27911  nlfnval  29664  padct  30481  tocyc01  30810  cycpmconjslem2  30847  indf1ofs  31395  ismbfm  31620  issibf  31701  sitgfval  31709  eulerpartlemelr  31725  eulerpartleme  31731  eulerpartlemo  31733  eulerpartlemt0  31737  eulerpartlemt  31739  eulerpartgbij  31740  eulerpartlemr  31742  eulerpartlemgs2  31748  eulerpartlemn  31749  eulerpart  31750  funen1cnv  32467  iscvm  32619  elmpst  32896  elsymrels2  35949  elsymrels4  35951  symreleq  35954  elrefsymrels2  35965  eleqvrels2  35987  eldisjs  36115  lkrval  36384  ltrncnvnid  37423  cdlemkuu  38191  pw2f1o2val  39980  pwfi2f1o  40040  clcnvlem  40323  rfovcnvf1od  40705  fsovrfovd  40710  issmflem  43361  isrngisom  44520