Theorem difeq2 3873

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1631   ∈ wcel 2145  {crab 3065   ∖ cdif 3720

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-ral 3066  df-rab 3070  df-dif 3726

This theorem is referenced by:  difeq12  3874  difeq2i  3876  difeq2d  3879  symdifeq1  3995  ssdifim  4011  disjdif2  4189  ssdifeq0  4193  sorpsscmpl  7095  2oconcl  7737  oev  7748  sbthlem2  8227  sbth  8236  infdiffi  8719  fin1ai  9317  fin23lem7  9340  fin23lem11  9341  compsscnv  9395  isf34lem1  9396  compss  9400  isf34lem4  9401  fin1a2lem7  9430  pwfseqlem4a  9685  pwfseqlem4  9686  efgmval  18332  efgi  18339  frgpuptinv  18391  gsumcllem  18516  gsumzaddlem  18528  fctop  21029  cctop  21031  iscld  21052  clsval2  21075  opncldf1  21109  opncldf2  21110  opncldf3  21111  indiscld  21116  mretopd  21117  restcld  21197  lecldbas  21244  pnrmopn  21368  hauscmplem  21430  elpt  21596  elptr  21597  cfinfil  21917  csdfil  21918  ufilss  21929  filufint  21944  cfinufil  21952  ufinffr  21953  ufilen  21954  prdsxmslem2  22554  lebnumlem1  22980  bcth3  23347  ismbl  23514  ishpg  25872  frgrwopregasn  27498  frgrwopregbsn  27499  disjdifprg  29726  0elsiga  30517  prsiga  30534  sigaclci  30535  difelsiga  30536  unelldsys  30561  sigapildsyslem  30564  sigapildsys  30565  ldgenpisyslem1  30566  isros  30571  unelros  30574  difelros  30575  inelsros  30581  diffiunisros  30582  rossros  30583  elcarsg  30707  ballotlemfval  30891  ballotlemgval  30925  kur14lem1  31526  topdifinffinlem  33532  topdifinffin  33533  dssmapfv3d  38839  dssmapnvod  38840  clsk3nimkb  38864  ntrclsneine0lem  38888  ntrclsk2  38892  ntrclskb  38893  ntrclsk13  38895  ntrclsk4  38896  prsal  41055  saldifcl  41056  salexct  41069  salexct2  41074  salexct3  41077  salgencntex  41078  salgensscntex  41079  caragenel  41229