Theorem cnveq 5744

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 5743	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵)
2		cnvss 5743	. . 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 1537   ⊆ wss 3936  ^◡ccnv 5554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-in 3943  df-ss 3952  df-br 5067  df-opab 5129  df-cnv 5563

This theorem is referenced by:  cnveqi  5745  cnveqd  5746  rneq  5806  cnveqb  6053  predeq123  6149  f1eq1  6570  f1ssf1  6646  f1o00  6649  foeqcnvco  7056  funcnvuni  7636  tposfn2  7914  ereq1  8296  infeq3  8944  1arith  16263  vdwmc  16314  vdwnnlem1  16331  ramub2  16350  rami  16351  isps  17812  istsr  17827  isdir  17842  isrim0  19475  psrbag  20144  psrbaglefi  20152  iscn  21843  ishmeo  22367  symgtgp  22714  ustincl  22816  ustdiag  22817  ustinvel  22818  ustexhalf  22819  ustexsym  22824  ust0  22828  isi1f  24275  itg1val  24284  fta1lem  24896  fta1  24897  vieta1lem2  24900  vieta1  24901  sqff1o  25759  istrl  27478  isspth  27505  upgrwlkdvspth  27520  uhgrwkspthlem1  27534  0spth  27905  nlfnval  29658  padct  30455  tocyc01  30760  cycpmconjslem2  30797  indf1ofs  31285  ismbfm  31510  issibf  31591  sitgfval  31599  eulerpartlemelr  31615  eulerpartleme  31621  eulerpartlemo  31623  eulerpartlemt0  31627  eulerpartlemt  31629  eulerpartgbij  31630  eulerpartlemr  31632  eulerpartlemgs2  31638  eulerpartlemn  31639  eulerpart  31640  funen1cnv  32357  iscvm  32506  elmpst  32783  elsymrels2  35804  elsymrels4  35806  symreleq  35809  elrefsymrels2  35820  eleqvrels2  35842  eldisjs  35970  lkrval  36239  ltrncnvnid  37278  cdlemkuu  38046  pw2f1o2val  39656  pwfi2f1o  39716  clcnvlem  40003  rfovcnvf1od  40370  fsovrfovd  40375  issmflem  43024  isrngisom  44187