Theorem difeq2 4115

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 2822	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	notbid 317	. . 3 ⊢ (𝐴 = 𝐵 → (¬ 𝑥 ∈ 𝐴 ↔ ¬ 𝑥 ∈ 𝐵))
3	2	rabbidv 3440	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴} = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵})
4		dfdif2 3956	. 2 ⊢ (𝐶 ∖ 𝐴) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴}
5		dfdif2 3956	. 2 ⊢ (𝐶 ∖ 𝐵) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵}
6	3, 4, 5	3eqtr4g 2797	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ∈ wcel 2106  {crab 3432   ∖ cdif 3944

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-dif 3950

This theorem is referenced by:  difeq12  4116  difeq2i  4118  difeq2d  4121  symdifeq1  4243  ssdifim  4261  disjdif2  4478  ssdifeq0  4485  sorpsscmpl  7720  2oconcl  8499  oev  8510  sbthlem2  9080  sbth  9089  sbthfi  9198  infdiffi  9649  fin1ai  10284  fin23lem7  10307  fin23lem11  10308  compsscnv  10362  isf34lem1  10363  compss  10367  isf34lem4  10368  fin1a2lem7  10397  pwfseqlem4a  10652  pwfseqlem4  10653  efgmval  19574  efgi  19581  frgpuptinv  19633  gsumcllem  19770  gsumzaddlem  19783  selvfval  21671  fctop  22498  cctop  22500  iscld  22522  clsval2  22545  opncldf1  22579  opncldf2  22580  opncldf3  22581  indiscld  22586  mretopd  22587  restcld  22667  lecldbas  22714  pnrmopn  22838  hauscmplem  22901  elpt  23067  elptr  23068  cfinfil  23388  csdfil  23389  ufilss  23400  filufint  23415  cfinufil  23423  ufinffr  23424  ufilen  23425  prdsxmslem2  24029  lebnumlem1  24468  bcth3  24839  ismbl  25034  ishpg  27999  frgrwopregasn  29558  frgrwopregbsn  29559  disjdifprg  31793  0elsiga  33100  prsiga  33117  sigaclci  33118  difelsiga  33119  unelldsys  33144  sigapildsyslem  33147  sigapildsys  33148  ldgenpisyslem1  33149  isros  33154  unelros  33157  difelros  33158  inelsros  33164  diffiunisros  33165  rossros  33166  elcarsg  33292  ballotlemfval  33476  ballotlemgval  33510  kur14lem1  34185  topdifinffinlem  36216  topdifinffin  36217  oe0rif  42020  dssmapfv3d  42755  dssmapnvod  42756  clsk3nimkb  42776  ntrclsneine0lem  42800  ntrclsk2  42804  ntrclskb  42805  ntrclsk13  42807  ntrclsk4  42808  prsal  45020  saldifcl  45021  salexct  45036  salexct2  45041  salexct3  45044  salgencntex  45045  salgensscntex  45046  caragenel  45197  opncldeqv  47487