Theorem difeq2 4072

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ∈ wcel 2113  {crab 3399   ∖ cdif 3898

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 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-dif 3904

This theorem is referenced by:  difeq12  4073  difeq2i  4075  difeq2d  4078  symdifeq1  4207  ssdifim  4225  disjdif2  4432  ssdifeq0  4439  sorpsscmpl  7679  2oconcl  8430  oev  8441  sbthlem2  9016  sbth  9025  sbthfi  9123  infdiffi  9567  fin1ai  10203  fin23lem7  10226  fin23lem11  10227  compsscnv  10281  isf34lem1  10282  compss  10286  isf34lem4  10287  fin1a2lem7  10316  pwfseqlem4a  10572  pwfseqlem4  10573  efgmval  19641  efgi  19648  frgpuptinv  19700  gsumcllem  19837  gsumzaddlem  19850  selvfval  22077  fctop  22948  cctop  22950  iscld  22971  clsval2  22994  opncldf1  23028  opncldf2  23029  opncldf3  23030  indiscld  23035  mretopd  23036  restcld  23116  lecldbas  23163  pnrmopn  23287  hauscmplem  23350  elpt  23516  elptr  23517  cfinfil  23837  csdfil  23838  ufilss  23849  filufint  23864  cfinufil  23872  ufinffr  23873  ufilen  23874  prdsxmslem2  24473  lebnumlem1  24916  bcth3  25287  ismbl  25483  ishpg  28831  frgrwopregasn  30391  frgrwopregbsn  30392  disjdifprg  32650  0elsiga  34271  prsiga  34288  sigaclci  34289  difelsiga  34290  unelldsys  34315  sigapildsyslem  34318  sigapildsys  34319  ldgenpisyslem1  34320  isros  34325  unelros  34328  difelros  34329  inelsros  34335  diffiunisros  34336  rossros  34337  elcarsg  34462  ballotlemfval  34647  ballotlemgval  34681  kur14lem1  35400  topdifinffinlem  37552  topdifinffin  37553  oe0rif  43527  dssmapfv3d  44260  dssmapnvod  44261  clsk3nimkb  44281  ntrclsneine0lem  44305  ntrclsk2  44309  ntrclskb  44310  ntrclsk13  44312  ntrclsk4  44313  prsal  46562  saldifcl  46563  salexct  46578  salexct2  46583  salexct3  46586  salgencntex  46587  salgensscntex  46588  caragenel  46739  opncldeqv  49147