Theorem cnveq 5857

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ⊆ wss 3900  ^◡ccnv 5654

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ss 3901  df-br 5107  df-opab 5171  df-cnv 5663

This theorem is used by:  cnveqi  5858  cnveqd  5859  rneq  5924  predeq123  6320  f1eq1  6792  f1ssf1  6877  f1o00  6880  foeqcnvco  7328  funcnvuni  7965  tposfn2  8290  ereq1  8750  funen1cnv  9081  cnvfi  9216  infeq3  9497  1arith  17131  vdwmc  17182  vdwnnlem1  17199  ramub2  17218  rami  17219  isps  18768  istsr  18783  isdir  18798  isrngim  20702  isrim0  20740  psrbag  22252  psrbaglefi  22261  iscn  23580  ishmeo  24105  symgtgp  24452  ustincl  24554  ustdiag  24555  ustinvel  24556  ustexhalf  24557  ustexsym  24562  ust0  24566  isi1f  26022  itg1val  26031  fta1lem  26655  fta1  26656  vieta1lem2  26661  vieta1  26662  sqff1o  27536  istrl  30306  isspth  30334  upgrwlkdvspth  30352  uhgrwkspthlem1  30366  0spth  30744  nlfnval  32510  padct  33378  indf1ofs  33500  tocyc01  33746  cycpmconjslem2  33783  ismbfm  34951  issibf  35032  sitgfval  35040  eulerpartlemelr  35056  eulerpartleme  35062  eulerpartlemo  35064  eulerpartlemt0  35068  eulerpartlemt  35070  eulerpartgbij  35071  eulerpartlemr  35073  eulerpartlemgs2  35079  eulerpartlemn  35080  eulerpart  35081  gdlop6fv  35967  iscvm  36190  elmpst  36467  elsymrels2  39760  elsymrels4  39762  symreleq  39765  elrefsymrels2  39776  eleqvrels2  39799  eldisjs  39942  lkrval  40336  ltrncnvnid  41375  cdlemkuu  42143  pw2f1o2val  44237  pwfi2f1o  44289  clcnvlem  44813  rfovcnvf1od  45194  fsovrfovd  45199  issmflem  47940