Theorem difeq2 4060

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-dif 3892

This theorem is referenced by:  difeq12  4061  difeq2i  4063  difeq2d  4066  symdifeq1  4195  ssdifim  4213  disjdif2  4420  ssdifeq0  4426  sorpsscmpl  7688  2oconcl  8438  oev  8449  sbthlem2  9026  sbth  9035  sbthfi  9133  infdiffi  9579  fin1ai  10215  fin23lem7  10238  fin23lem11  10239  compsscnv  10293  isf34lem1  10294  compss  10298  isf34lem4  10299  fin1a2lem7  10328  pwfseqlem4a  10584  pwfseqlem4  10585  efgmval  19687  efgi  19694  frgpuptinv  19746  gsumcllem  19883  gsumzaddlem  19896  selvfval  22100  fctop  22969  cctop  22971  iscld  22992  clsval2  23015  opncldf1  23049  opncldf2  23050  opncldf3  23051  indiscld  23056  mretopd  23057  restcld  23137  lecldbas  23184  pnrmopn  23308  hauscmplem  23371  elpt  23537  elptr  23538  cfinfil  23858  csdfil  23859  ufilss  23870  filufint  23885  cfinufil  23893  ufinffr  23894  ufilen  23895  prdsxmslem2  24494  lebnumlem1  24928  bcth3  25298  ismbl  25493  ishpg  28827  frgrwopregasn  30386  frgrwopregbsn  30387  disjdifprg  32645  0elsiga  34258  prsiga  34275  sigaclci  34276  difelsiga  34277  unelldsys  34302  sigapildsyslem  34305  sigapildsys  34306  ldgenpisyslem1  34307  isros  34312  unelros  34315  difelros  34316  inelsros  34322  diffiunisros  34323  rossros  34324  elcarsg  34449  ballotlemfval  34634  ballotlemgval  34668  kur14lem1  35388  topdifinffinlem  37663  topdifinffin  37664  oe0rif  43713  dssmapfv3d  44446  dssmapnvod  44447  clsk3nimkb  44467  ntrclsneine0lem  44491  ntrclsk2  44495  ntrclskb  44496  ntrclsk13  44498  ntrclsk4  44499  prsal  46746  saldifcl  46747  salexct  46762  salexct2  46767  salexct3  46770  salgencntex  46771  salgensscntex  46772  caragenel  46923  opncldeqv  49377