Theorem difeq2 4130

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 2828	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	notbid 318	. . 3 ⊢ (𝐴 = 𝐵 → (¬ 𝑥 ∈ 𝐴 ↔ ¬ 𝑥 ∈ 𝐵))
3	2	rabbidv 3441	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴} = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵})
4		dfdif2 3972	. 2 ⊢ (𝐶 ∖ 𝐴) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴}
5		dfdif2 3972	. 2 ⊢ (𝐶 ∖ 𝐵) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵}
6	3, 4, 5	3eqtr4g 2800	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ∈ wcel 2106  {crab 3433   ∖ cdif 3960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-dif 3966

This theorem is referenced by:  difeq12  4131  difeq2i  4133  difeq2d  4136  symdifeq1  4261  ssdifim  4279  disjdif2  4486  ssdifeq0  4493  sorpsscmpl  7753  2oconcl  8540  oev  8551  sbthlem2  9123  sbth  9132  sbthfi  9237  infdiffi  9696  fin1ai  10331  fin23lem7  10354  fin23lem11  10355  compsscnv  10409  isf34lem1  10410  compss  10414  isf34lem4  10415  fin1a2lem7  10444  pwfseqlem4a  10699  pwfseqlem4  10700  efgmval  19745  efgi  19752  frgpuptinv  19804  gsumcllem  19941  gsumzaddlem  19954  selvfval  22156  fctop  23027  cctop  23029  iscld  23051  clsval2  23074  opncldf1  23108  opncldf2  23109  opncldf3  23110  indiscld  23115  mretopd  23116  restcld  23196  lecldbas  23243  pnrmopn  23367  hauscmplem  23430  elpt  23596  elptr  23597  cfinfil  23917  csdfil  23918  ufilss  23929  filufint  23944  cfinufil  23952  ufinffr  23953  ufilen  23954  prdsxmslem2  24558  lebnumlem1  25007  bcth3  25379  ismbl  25575  ishpg  28782  frgrwopregasn  30345  frgrwopregbsn  30346  disjdifprg  32595  0elsiga  34095  prsiga  34112  sigaclci  34113  difelsiga  34114  unelldsys  34139  sigapildsyslem  34142  sigapildsys  34143  ldgenpisyslem1  34144  isros  34149  unelros  34152  difelros  34153  inelsros  34159  diffiunisros  34160  rossros  34161  elcarsg  34287  ballotlemfval  34471  ballotlemgval  34505  kur14lem1  35191  topdifinffinlem  37330  topdifinffin  37331  oe0rif  43275  dssmapfv3d  44009  dssmapnvod  44010  clsk3nimkb  44030  ntrclsneine0lem  44054  ntrclsk2  44058  ntrclskb  44059  ntrclsk13  44061  ntrclsk4  44062  prsal  46274  saldifcl  46275  salexct  46290  salexct2  46295  salexct3  46298  salgencntex  46299  salgensscntex  46300  caragenel  46451  opncldeqv  48698