Theorem difeq2 3722

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 2690	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	notbid 308	. . 3 ⊢ (𝐴 = 𝐵 → (¬ 𝑥 ∈ 𝐴 ↔ ¬ 𝑥 ∈ 𝐵))
3	2	rabbidv 3189	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴} = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵})
4		dfdif2 3583	. 2 ⊢ (𝐶 ∖ 𝐴) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴}
5		dfdif2 3583	. 2 ⊢ (𝐶 ∖ 𝐵) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵}
6	3, 4, 5	3eqtr4g 2681	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1483   ∈ wcel 1990  {crab 2916   ∖ cdif 3571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-ral 2917  df-rab 2921  df-dif 3577

This theorem is referenced by:  difeq12  3723  difeq2i  3725  difeq2d  3728  symdifeq1  3846  ssdifim  3862  disjdif2  4047  ssdifeq0  4051  sorpsscmpl  6948  2oconcl  7583  oev  7594  sbthlem2  8071  sbth  8080  infdiffi  8555  fin1ai  9115  fin23lem7  9138  fin23lem11  9139  compsscnv  9193  isf34lem1  9194  compss  9198  isf34lem4  9199  fin1a2lem7  9228  pwfseqlem4a  9483  pwfseqlem4  9484  efgmval  18125  efgi  18132  frgpuptinv  18184  gsumcllem  18309  gsumzaddlem  18321  fctop  20808  cctop  20810  iscld  20831  clsval2  20854  opncldf1  20888  opncldf2  20889  opncldf3  20890  indiscld  20895  mretopd  20896  restcld  20976  lecldbas  21023  pnrmopn  21147  hauscmplem  21209  elpt  21375  elptr  21376  cfinfil  21697  csdfil  21698  ufilss  21709  filufint  21724  cfinufil  21732  ufinffr  21733  ufilen  21734  prdsxmslem2  22334  lebnumlem1  22760  bcth3  23128  ismbl  23294  ishpg  25651  frgrwopregasn  27180  frgrwopregbsn  27181  disjdifprg  29388  0elsiga  30177  prsiga  30194  sigaclci  30195  difelsiga  30196  unelldsys  30221  sigapildsyslem  30224  sigapildsys  30225  ldgenpisyslem1  30226  isros  30231  unelros  30234  difelros  30235  inelsros  30241  diffiunisros  30242  rossros  30243  elcarsg  30367  ballotlemfval  30551  ballotlemgval  30585  kur14lem1  31188  topdifinffinlem  33195  topdifinffin  33196  dssmapfv3d  38313  dssmapnvod  38314  clsk3nimkb  38338  ntrclsneine0lem  38362  ntrclsk2  38366  ntrclskb  38367  ntrclsk13  38369  ntrclsk4  38370  prsal  40538  saldifcl  40539  salexct  40552  salexct2  40557  salexct3  40560  salgencntex  40561  salgensscntex  40562  caragenel  40709