Theorem difeq2 4067

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ∈ wcel 2111  {crab 3395   ∖ cdif 3894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-dif 3900

This theorem is referenced by:  difeq12  4068  difeq2i  4070  difeq2d  4073  symdifeq1  4202  ssdifim  4220  disjdif2  4427  ssdifeq0  4434  sorpsscmpl  7667  2oconcl  8418  oev  8429  sbthlem2  9001  sbth  9010  sbthfi  9108  infdiffi  9548  fin1ai  10184  fin23lem7  10207  fin23lem11  10208  compsscnv  10262  isf34lem1  10263  compss  10267  isf34lem4  10268  fin1a2lem7  10297  pwfseqlem4a  10552  pwfseqlem4  10553  efgmval  19624  efgi  19631  frgpuptinv  19683  gsumcllem  19820  gsumzaddlem  19833  selvfval  22049  fctop  22919  cctop  22921  iscld  22942  clsval2  22965  opncldf1  22999  opncldf2  23000  opncldf3  23001  indiscld  23006  mretopd  23007  restcld  23087  lecldbas  23134  pnrmopn  23258  hauscmplem  23321  elpt  23487  elptr  23488  cfinfil  23808  csdfil  23809  ufilss  23820  filufint  23835  cfinufil  23843  ufinffr  23844  ufilen  23845  prdsxmslem2  24444  lebnumlem1  24887  bcth3  25258  ismbl  25454  ishpg  28737  frgrwopregasn  30296  frgrwopregbsn  30297  disjdifprg  32555  0elsiga  34127  prsiga  34144  sigaclci  34145  difelsiga  34146  unelldsys  34171  sigapildsyslem  34174  sigapildsys  34175  ldgenpisyslem1  34176  isros  34181  unelros  34184  difelros  34185  inelsros  34191  diffiunisros  34192  rossros  34193  elcarsg  34318  ballotlemfval  34503  ballotlemgval  34537  kur14lem1  35250  topdifinffinlem  37391  topdifinffin  37392  oe0rif  43388  dssmapfv3d  44122  dssmapnvod  44123  clsk3nimkb  44143  ntrclsneine0lem  44167  ntrclsk2  44171  ntrclskb  44172  ntrclsk13  44174  ntrclsk4  44175  prsal  46426  saldifcl  46427  salexct  46442  salexct2  46447  salexct3  46450  salgencntex  46451  salgensscntex  46452  caragenel  46603  opncldeqv  49012