Theorem difeq2 4119

Description: Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

Ref	Expression
difeq2	⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))

Proof of Theorem difeq2

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq2 2829	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	notbid 318	. . 3 ⊢ (𝐴 = 𝐵 → (¬ 𝑥 ∈ 𝐴 ↔ ¬ 𝑥 ∈ 𝐵))
3	2	rabbidv 3443	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴} = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵})
4		dfdif2 3959	. 2 ⊢ (𝐶 ∖ 𝐴) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴}
5		dfdif2 3959	. 2 ⊢ (𝐶 ∖ 𝐵) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵}
6	3, 4, 5	3eqtr4g 2801	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ∈ wcel 2107  {crab 3435   ∖ cdif 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-dif 3953

This theorem is referenced by:  difeq12  4120  difeq2i  4122  difeq2d  4125  symdifeq1  4254  ssdifim  4272  disjdif2  4479  ssdifeq0  4486  sorpsscmpl  7755  2oconcl  8542  oev  8553  sbthlem2  9125  sbth  9134  sbthfi  9240  infdiffi  9699  fin1ai  10334  fin23lem7  10357  fin23lem11  10358  compsscnv  10412  isf34lem1  10413  compss  10417  isf34lem4  10418  fin1a2lem7  10447  pwfseqlem4a  10702  pwfseqlem4  10703  efgmval  19731  efgi  19738  frgpuptinv  19790  gsumcllem  19927  gsumzaddlem  19940  selvfval  22139  fctop  23012  cctop  23014  iscld  23036  clsval2  23059  opncldf1  23093  opncldf2  23094  opncldf3  23095  indiscld  23100  mretopd  23101  restcld  23181  lecldbas  23228  pnrmopn  23352  hauscmplem  23415  elpt  23581  elptr  23582  cfinfil  23902  csdfil  23903  ufilss  23914  filufint  23929  cfinufil  23937  ufinffr  23938  ufilen  23939  prdsxmslem2  24543  lebnumlem1  24994  bcth3  25366  ismbl  25562  ishpg  28768  frgrwopregasn  30336  frgrwopregbsn  30337  disjdifprg  32589  0elsiga  34116  prsiga  34133  sigaclci  34134  difelsiga  34135  unelldsys  34160  sigapildsyslem  34163  sigapildsys  34164  ldgenpisyslem1  34165  isros  34170  unelros  34173  difelros  34174  inelsros  34180  diffiunisros  34181  rossros  34182  elcarsg  34308  ballotlemfval  34493  ballotlemgval  34527  kur14lem1  35212  topdifinffinlem  37349  topdifinffin  37350  oe0rif  43303  dssmapfv3d  44037  dssmapnvod  44038  clsk3nimkb  44058  ntrclsneine0lem  44082  ntrclsk2  44086  ntrclskb  44087  ntrclsk13  44089  ntrclsk4  44090  prsal  46338  saldifcl  46339  salexct  46354  salexct2  46359  salexct3  46362  salgencntex  46363  salgensscntex  46364  caragenel  46515  opncldeqv  48806