Theorem difeq2 4100

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ∈ wcel 2109  {crab 3420   ∖ cdif 3928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-dif 3934

This theorem is referenced by:  difeq12  4101  difeq2i  4103  difeq2d  4106  symdifeq1  4235  ssdifim  4253  disjdif2  4460  ssdifeq0  4467  sorpsscmpl  7733  2oconcl  8520  oev  8531  sbthlem2  9103  sbth  9112  sbthfi  9218  infdiffi  9677  fin1ai  10312  fin23lem7  10335  fin23lem11  10336  compsscnv  10390  isf34lem1  10391  compss  10395  isf34lem4  10396  fin1a2lem7  10425  pwfseqlem4a  10680  pwfseqlem4  10681  efgmval  19698  efgi  19705  frgpuptinv  19757  gsumcllem  19894  gsumzaddlem  19907  selvfval  22077  fctop  22947  cctop  22949  iscld  22970  clsval2  22993  opncldf1  23027  opncldf2  23028  opncldf3  23029  indiscld  23034  mretopd  23035  restcld  23115  lecldbas  23162  pnrmopn  23286  hauscmplem  23349  elpt  23515  elptr  23516  cfinfil  23836  csdfil  23837  ufilss  23848  filufint  23863  cfinufil  23871  ufinffr  23872  ufilen  23873  prdsxmslem2  24473  lebnumlem1  24916  bcth3  25288  ismbl  25484  ishpg  28743  frgrwopregasn  30302  frgrwopregbsn  30303  disjdifprg  32561  0elsiga  34150  prsiga  34167  sigaclci  34168  difelsiga  34169  unelldsys  34194  sigapildsyslem  34197  sigapildsys  34198  ldgenpisyslem1  34199  isros  34204  unelros  34207  difelros  34208  inelsros  34214  diffiunisros  34215  rossros  34216  elcarsg  34342  ballotlemfval  34527  ballotlemgval  34561  kur14lem1  35233  topdifinffinlem  37370  topdifinffin  37371  oe0rif  43284  dssmapfv3d  44018  dssmapnvod  44019  clsk3nimkb  44039  ntrclsneine0lem  44063  ntrclsk2  44067  ntrclskb  44068  ntrclsk13  44070  ntrclsk4  44071  prsal  46327  saldifcl  46328  salexct  46343  salexct2  46348  salexct3  46351  salgencntex  46352  salgensscntex  46353  caragenel  46504  opncldeqv  48856