Theorem difeq2 4095

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 2903	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	notbid 320	. . 3 ⊢ (𝐴 = 𝐵 → (¬ 𝑥 ∈ 𝐴 ↔ ¬ 𝑥 ∈ 𝐵))
3	2	rabbidv 3482	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴} = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵})
4		dfdif2 3947	. 2 ⊢ (𝐶 ∖ 𝐴) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴}
5		dfdif2 3947	. 2 ⊢ (𝐶 ∖ 𝐵) = {𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵}
6	3, 4, 5	3eqtr4g 2883	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ∈ wcel 2114  {crab 3144   ∖ cdif 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-rab 3149  df-dif 3941

This theorem is referenced by:  difeq12  4096  difeq2i  4098  difeq2d  4101  symdifeq1  4223  ssdifim  4241  disjdif2  4430  ssdifeq0  4434  sorpsscmpl  7462  2oconcl  8130  oev  8141  sbthlem2  8630  sbth  8639  infdiffi  9123  fin1ai  9717  fin23lem7  9740  fin23lem11  9741  compsscnv  9795  isf34lem1  9796  compss  9800  isf34lem4  9801  fin1a2lem7  9830  pwfseqlem4a  10085  pwfseqlem4  10086  efgmval  18840  efgi  18847  frgpuptinv  18899  gsumcllem  19030  gsumzaddlem  19043  selvfval  20332  fctop  21614  cctop  21616  iscld  21637  clsval2  21660  opncldf1  21694  opncldf2  21695  opncldf3  21696  indiscld  21701  mretopd  21702  restcld  21782  lecldbas  21829  pnrmopn  21953  hauscmplem  22016  elpt  22182  elptr  22183  cfinfil  22503  csdfil  22504  ufilss  22515  filufint  22530  cfinufil  22538  ufinffr  22539  ufilen  22540  prdsxmslem2  23141  lebnumlem1  23567  bcth3  23936  ismbl  24129  ishpg  26547  frgrwopregasn  28097  frgrwopregbsn  28098  disjdifprg  30327  0elsiga  31375  prsiga  31392  sigaclci  31393  difelsiga  31394  unelldsys  31419  sigapildsyslem  31422  sigapildsys  31423  ldgenpisyslem1  31424  isros  31429  unelros  31432  difelros  31433  inelsros  31439  diffiunisros  31440  rossros  31441  elcarsg  31565  ballotlemfval  31749  ballotlemgval  31783  kur14lem1  32455  topdifinffinlem  34630  topdifinffin  34631  dssmapfv3d  40372  dssmapnvod  40373  clsk3nimkb  40397  ntrclsneine0lem  40421  ntrclsk2  40425  ntrclskb  40426  ntrclsk13  40428  ntrclsk4  40429  prsal  42610  saldifcl  42611  salexct  42624  salexct2  42629  salexct3  42632  salgencntex  42633  salgensscntex  42634  caragenel  42784