Theorem cnveq 5887

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ⊆ wss 3963  ^◡ccnv 5688

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ss 3980  df-br 5149  df-opab 5211  df-cnv 5697

This theorem is referenced by:  cnveqi  5888  cnveqd  5889  rneq  5950  cnveqb  6218  predeq123  6324  f1eq1  6800  f1ssf1  6881  f1o00  6884  foeqcnvco  7320  funcnvuni  7955  tposfn2  8272  ereq1  8751  cnvfi  9215  infeq3  9518  1arith  16961  vdwmc  17012  vdwnnlem1  17029  ramub2  17048  rami  17049  isps  18626  istsr  18641  isdir  18656  isrngim  20462  isrim0OLD  20498  isrim0  20500  psrbag  21955  psrbaglefi  21964  iscn  23259  ishmeo  23783  symgtgp  24130  ustincl  24232  ustdiag  24233  ustinvel  24234  ustexhalf  24235  ustexsym  24240  ust0  24244  isi1f  25723  itg1val  25732  fta1lem  26364  fta1  26365  vieta1lem2  26368  vieta1  26369  sqff1o  27240  istrl  29729  isspth  29757  upgrwlkdvspth  29772  uhgrwkspthlem1  29786  0spth  30155  nlfnval  31910  padct  32737  tocyc01  33121  cycpmconjslem2  33158  indf1ofs  34007  ismbfm  34232  issibf  34315  sitgfval  34323  eulerpartlemelr  34339  eulerpartleme  34345  eulerpartlemo  34347  eulerpartlemt0  34351  eulerpartlemt  34353  eulerpartgbij  34354  eulerpartlemr  34356  eulerpartlemgs2  34362  eulerpartlemn  34363  eulerpart  34364  funen1cnv  35081  iscvm  35244  elmpst  35521  elsymrels2  38535  elsymrels4  38537  symreleq  38540  elrefsymrels2  38551  eleqvrels2  38574  eldisjs  38704  lkrval  39070  ltrncnvnid  40110  cdlemkuu  40878  pw2f1o2val  43028  pwfi2f1o  43085  clcnvlem  43613  rfovcnvf1od  43994  fsovrfovd  43999  issmflem  46683