Theorem difeq2 4074

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 2826	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	notbid 318	. . 3 ⊢ (𝐴 = 𝐵 → (¬ 𝑥 ∈ 𝐴 ↔ ¬ 𝑥 ∈ 𝐵))
3	2	rabbidv 3408	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴} = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵})
4		dfdif2 3912	. 2 ⊢ (𝐶 ∖ 𝐴) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴}
5		dfdif2 3912	. 2 ⊢ (𝐶 ∖ 𝐵) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵}
6	3, 4, 5	3eqtr4g 2797	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ∈ wcel 2114  {crab 3401   ∖ cdif 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-dif 3906

This theorem is referenced by:  difeq12  4075  difeq2i  4077  difeq2d  4080  symdifeq1  4209  ssdifim  4227  disjdif2  4434  ssdifeq0  4441  sorpsscmpl  7689  2oconcl  8440  oev  8451  sbthlem2  9028  sbth  9037  sbthfi  9135  infdiffi  9579  fin1ai  10215  fin23lem7  10238  fin23lem11  10239  compsscnv  10293  isf34lem1  10294  compss  10298  isf34lem4  10299  fin1a2lem7  10328  pwfseqlem4a  10584  pwfseqlem4  10585  efgmval  19653  efgi  19660  frgpuptinv  19712  gsumcllem  19849  gsumzaddlem  19862  selvfval  22089  fctop  22960  cctop  22962  iscld  22983  clsval2  23006  opncldf1  23040  opncldf2  23041  opncldf3  23042  indiscld  23047  mretopd  23048  restcld  23128  lecldbas  23175  pnrmopn  23299  hauscmplem  23362  elpt  23528  elptr  23529  cfinfil  23849  csdfil  23850  ufilss  23861  filufint  23876  cfinufil  23884  ufinffr  23885  ufilen  23886  prdsxmslem2  24485  lebnumlem1  24928  bcth3  25299  ismbl  25495  ishpg  28843  frgrwopregasn  30403  frgrwopregbsn  30404  disjdifprg  32662  0elsiga  34292  prsiga  34309  sigaclci  34310  difelsiga  34311  unelldsys  34336  sigapildsyslem  34339  sigapildsys  34340  ldgenpisyslem1  34341  isros  34346  unelros  34349  difelros  34350  inelsros  34356  diffiunisros  34357  rossros  34358  elcarsg  34483  ballotlemfval  34668  ballotlemgval  34702  kur14lem1  35422  topdifinffinlem  37602  topdifinffin  37603  oe0rif  43642  dssmapfv3d  44375  dssmapnvod  44376  clsk3nimkb  44396  ntrclsneine0lem  44420  ntrclsk2  44424  ntrclskb  44425  ntrclsk13  44427  ntrclsk4  44428  prsal  46676  saldifcl  46677  salexct  46692  salexct2  46697  salexct3  46700  salgencntex  46701  salgensscntex  46702  caragenel  46853  opncldeqv  49261