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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ∈ wcel 2104  {crab 3430   ∖ cdif 3944

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-dif 3950

This theorem is referenced by:  difeq12  4116  difeq2i  4118  difeq2d  4121  symdifeq1  4243  ssdifim  4261  disjdif2  4478  ssdifeq0  4485  sorpsscmpl  7726  2oconcl  8505  oev  8516  sbthlem2  9086  sbth  9095  sbthfi  9204  infdiffi  9655  fin1ai  10290  fin23lem7  10313  fin23lem11  10314  compsscnv  10368  isf34lem1  10369  compss  10373  isf34lem4  10374  fin1a2lem7  10403  pwfseqlem4a  10658  pwfseqlem4  10659  efgmval  19621  efgi  19628  frgpuptinv  19680  gsumcllem  19817  gsumzaddlem  19830  selvfval  21899  fctop  22727  cctop  22729  iscld  22751  clsval2  22774  opncldf1  22808  opncldf2  22809  opncldf3  22810  indiscld  22815  mretopd  22816  restcld  22896  lecldbas  22943  pnrmopn  23067  hauscmplem  23130  elpt  23296  elptr  23297  cfinfil  23617  csdfil  23618  ufilss  23629  filufint  23644  cfinufil  23652  ufinffr  23653  ufilen  23654  prdsxmslem2  24258  lebnumlem1  24707  bcth3  25079  ismbl  25275  ishpg  28277  frgrwopregasn  29836  frgrwopregbsn  29837  disjdifprg  32073  0elsiga  33410  prsiga  33427  sigaclci  33428  difelsiga  33429  unelldsys  33454  sigapildsyslem  33457  sigapildsys  33458  ldgenpisyslem1  33459  isros  33464  unelros  33467  difelros  33468  inelsros  33474  diffiunisros  33475  rossros  33476  elcarsg  33602  ballotlemfval  33786  ballotlemgval  33820  kur14lem1  34495  topdifinffinlem  36531  topdifinffin  36532  oe0rif  42337  dssmapfv3d  43072  dssmapnvod  43073  clsk3nimkb  43093  ntrclsneine0lem  43117  ntrclsk2  43121  ntrclskb  43122  ntrclsk13  43124  ntrclsk4  43125  prsal  45332  saldifcl  45333  salexct  45348  salexct2  45353  salexct3  45356  salgencntex  45357  salgensscntex  45358  caragenel  45509  opncldeqv  47621