Theorem difeq2 4061

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 3397	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴} = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵})
4		dfdif2 3899	. 2 ⊢ (𝐶 ∖ 𝐴) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴}
5		dfdif2 3899	. 2 ⊢ (𝐶 ∖ 𝐵) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵}
6	3, 4, 5	3eqtr4g 2797	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))

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

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 3391  df-dif 3893

This theorem is referenced by:  difeq12  4062  difeq2i  4064  difeq2d  4067  symdifeq1  4196  ssdifim  4214  disjdif2  4421  ssdifeq0  4427  sorpsscmpl  7682  2oconcl  8432  oev  8443  sbthlem2  9020  sbth  9029  sbthfi  9127  infdiffi  9573  fin1ai  10209  fin23lem7  10232  fin23lem11  10233  compsscnv  10287  isf34lem1  10288  compss  10292  isf34lem4  10293  fin1a2lem7  10322  pwfseqlem4a  10578  pwfseqlem4  10579  efgmval  19681  efgi  19688  frgpuptinv  19740  gsumcllem  19877  gsumzaddlem  19890  selvfval  22113  fctop  22982  cctop  22984  iscld  23005  clsval2  23028  opncldf1  23062  opncldf2  23063  opncldf3  23064  indiscld  23069  mretopd  23070  restcld  23150  lecldbas  23197  pnrmopn  23321  hauscmplem  23384  elpt  23550  elptr  23551  cfinfil  23871  csdfil  23872  ufilss  23883  filufint  23898  cfinufil  23906  ufinffr  23907  ufilen  23908  prdsxmslem2  24507  lebnumlem1  24941  bcth3  25311  ismbl  25506  ishpg  28844  frgrwopregasn  30404  frgrwopregbsn  30405  disjdifprg  32663  0elsiga  34277  prsiga  34294  sigaclci  34295  difelsiga  34296  unelldsys  34321  sigapildsyslem  34324  sigapildsys  34325  ldgenpisyslem1  34326  isros  34331  unelros  34334  difelros  34335  inelsros  34341  diffiunisros  34342  rossros  34343  elcarsg  34468  ballotlemfval  34653  ballotlemgval  34687  kur14lem1  35407  topdifinffinlem  37680  topdifinffin  37681  oe0rif  43734  dssmapfv3d  44467  dssmapnvod  44468  clsk3nimkb  44488  ntrclsneine0lem  44512  ntrclsk2  44516  ntrclskb  44517  ntrclsk13  44519  ntrclsk4  44520  prsal  46767  saldifcl  46768  salexct  46783  salexct2  46788  salexct3  46791  salgencntex  46792  salgensscntex  46793  caragenel  46944  opncldeqv  49392