Theorem difeq2 3684

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 2677	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	notbid 307	. . 3 ⊢ (𝐴 = 𝐵 → (¬ 𝑥 ∈ 𝐴 ↔ ¬ 𝑥 ∈ 𝐵))
3	2	rabbidv 3164	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴} = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵})
4		dfdif2 3549	. 2 ⊢ (𝐶 ∖ 𝐴) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴}
5		dfdif2 3549	. 2 ⊢ (𝐶 ∖ 𝐵) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵}
6	3, 4, 5	3eqtr4g 2669	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ∈ wcel 1977  {crab 2900   ∖ cdif 3537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-ral 2901  df-rab 2905  df-dif 3543

This theorem is referenced by:  difeq12  3685  difeq2i  3687  difeq2d  3690  symdifeq1  3808  disjdif2  3999  ssdifeq0  4003  sorpsscmpl  6846  2oconcl  7470  oev  7481  sbthlem2  7956  sbth  7965  infdiffi  8438  fin1ai  8998  fin23lem7  9021  fin23lem11  9022  compsscnv  9076  isf34lem1  9077  compss  9081  isf34lem4  9082  fin1a2lem7  9111  pwfseqlem4a  9362  pwfseqlem4  9363  efgmval  17948  efgi  17955  frgpuptinv  18007  gsumcllem  18132  gsumzaddlem  18144  fctop  20618  cctop  20620  iscld  20641  clsval2  20664  opncldf1  20698  opncldf2  20699  opncldf3  20700  indiscld  20705  mretopd  20706  restcld  20786  lecldbas  20833  pnrmopn  20957  hauscmplem  21019  elpt  21185  elptr  21186  cfinfil  21507  csdfil  21508  ufilss  21519  filufint  21534  cfinufil  21542  ufinffr  21543  ufilen  21544  prdsxmslem2  22144  lebnumlem1  22568  bcth3  22936  ismbl  23101  ishpg  25451  frgrawopreg1  26577  frgrawopreg2  26578  disjdifprg  28770  0elsiga  29504  prsiga  29521  sigaclci  29522  difelsiga  29523  unelldsys  29548  sigapildsyslem  29551  sigapildsys  29552  ldgenpisyslem1  29553  isros  29558  unelros  29561  difelros  29562  inelsros  29568  diffiunisros  29569  rossros  29570  elcarsg  29694  ballotlemfval  29878  ballotlemgval  29912  kur14lem1  30442  topdifinffinlem  32371  topdifinffin  32372  dssmapfv3d  37333  dssmapnvod  37334  clsk3nimkb  37358  ntrclsneine0lem  37382  ntrclsk2  37386  ntrclskb  37387  ntrclsk13  37389  ntrclsk4  37390  prsal  39214  saldifcl  39215  salexct  39228  salexct2  39233  salexct3  39236  salgencntex  39237  salgensscntex  39238  caragenel  39385  frgrwopreg1  41487  frgrwopreg2  41488