Theorem cnveq 5827

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ⊆ wss 3911  ^◡ccnv 5630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3928  df-br 5103  df-opab 5165  df-cnv 5639

This theorem is referenced by:  cnveqi  5828  cnveqd  5829  rneq  5889  cnveqb  6157  predeq123  6263  f1eq1  6733  f1ssf1  6814  f1o00  6817  foeqcnvco  7257  funcnvuni  7888  tposfn2  8204  ereq1  8655  cnvfi  9117  infeq3  9408  1arith  16874  vdwmc  16925  vdwnnlem1  16942  ramub2  16961  rami  16962  isps  18509  istsr  18524  isdir  18539  isrngim  20365  isrim0OLD  20401  isrim0  20403  psrbag  21859  psrbaglefi  21868  iscn  23155  ishmeo  23679  symgtgp  24026  ustincl  24128  ustdiag  24129  ustinvel  24130  ustexhalf  24131  ustexsym  24136  ust0  24140  isi1f  25608  itg1val  25617  fta1lem  26248  fta1  26249  vieta1lem2  26252  vieta1  26253  sqff1o  27125  istrl  29675  isspth  29702  upgrwlkdvspth  29719  uhgrwkspthlem1  29733  0spth  30105  nlfnval  31860  padct  32693  indf1ofs  32839  tocyc01  33090  cycpmconjslem2  33127  ismbfm  34234  issibf  34317  sitgfval  34325  eulerpartlemelr  34341  eulerpartleme  34347  eulerpartlemo  34349  eulerpartlemt0  34353  eulerpartlemt  34355  eulerpartgbij  34356  eulerpartlemr  34358  eulerpartlemgs2  34364  eulerpartlemn  34365  eulerpart  34366  funen1cnv  35071  iscvm  35239  elmpst  35516  elsymrels2  38537  elsymrels4  38539  symreleq  38542  elrefsymrels2  38553  eleqvrels2  38576  eldisjs  38707  lkrval  39074  ltrncnvnid  40114  cdlemkuu  40882  pw2f1o2val  43021  pwfi2f1o  43078  clcnvlem  43605  rfovcnvf1od  43986  fsovrfovd  43991  issmflem  46718