Theorem difeq2 4044

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 2878	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	notbid 321	. . 3 ⊢ (𝐴 = 𝐵 → (¬ 𝑥 ∈ 𝐴 ↔ ¬ 𝑥 ∈ 𝐵))
3	2	rabbidv 3427	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴} = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵})
4		dfdif2 3890	. 2 ⊢ (𝐶 ∖ 𝐴) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴}
5		dfdif2 3890	. 2 ⊢ (𝐶 ∖ 𝐵) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵}
6	3, 4, 5	3eqtr4g 2858	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   ∈ wcel 2111  {crab 3110   ∖ cdif 3878

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-dif 3884

This theorem is referenced by:  difeq12  4045  difeq2i  4047  difeq2d  4050  symdifeq1  4171  ssdifim  4189  disjdif2  4386  ssdifeq0  4390  sorpsscmpl  7440  2oconcl  8111  oev  8122  sbthlem2  8612  sbth  8621  infdiffi  9105  fin1ai  9704  fin23lem7  9727  fin23lem11  9728  compsscnv  9782  isf34lem1  9783  compss  9787  isf34lem4  9788  fin1a2lem7  9817  pwfseqlem4a  10072  pwfseqlem4  10073  efgmval  18830  efgi  18837  frgpuptinv  18889  gsumcllem  19021  gsumzaddlem  19034  selvfval  20789  fctop  21609  cctop  21611  iscld  21632  clsval2  21655  opncldf1  21689  opncldf2  21690  opncldf3  21691  indiscld  21696  mretopd  21697  restcld  21777  lecldbas  21824  pnrmopn  21948  hauscmplem  22011  elpt  22177  elptr  22178  cfinfil  22498  csdfil  22499  ufilss  22510  filufint  22525  cfinufil  22533  ufinffr  22534  ufilen  22535  prdsxmslem2  23136  lebnumlem1  23566  bcth3  23935  ismbl  24130  ishpg  26553  frgrwopregasn  28101  frgrwopregbsn  28102  disjdifprg  30338  0elsiga  31483  prsiga  31500  sigaclci  31501  difelsiga  31502  unelldsys  31527  sigapildsyslem  31530  sigapildsys  31531  ldgenpisyslem1  31532  isros  31537  unelros  31540  difelros  31541  inelsros  31547  diffiunisros  31548  rossros  31549  elcarsg  31673  ballotlemfval  31857  ballotlemgval  31891  kur14lem1  32566  topdifinffinlem  34764  topdifinffin  34765  dssmapfv3d  40720  dssmapnvod  40721  clsk3nimkb  40743  ntrclsneine0lem  40767  ntrclsk2  40771  ntrclskb  40772  ntrclsk13  40774  ntrclsk4  40775  prsal  42960  saldifcl  42961  salexct  42974  salexct2  42979  salexct3  42982  salgencntex  42983  salgensscntex  42984  caragenel  43134