Theorem difeq2 4075

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2143  {crab 3416   ∖ cdif 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-dif 3908

This theorem is referenced by:  difeq12  4076  difeq2i  4078  difeq2d  4081  symdifeq1  4208  ssdifim  4226  disjdif2  4441  ssdifeq0  4447  xpdifcnvepel  6166  sorpsscmpl  7731  2oconcl  8484  oev  8495  sbthlem2  9072  sbth  9081  sbthfi  9179  infdiffi  9623  fin1ai  10272  fin23lem7  10295  fin23lem11  10296  compsscnv  10350  isf34lem1  10351  compss  10355  isf34lem4  10356  fin1a2lem7  10385  pwfseqlem4a  10641  pwfseqlem4  10642  efgmval  19777  efgi  19784  frgpuptinv  19836  gsumcllem  19973  gsumzaddlem  19986  selvfval  22270  fctop  23161  cctop  23163  iscld  23184  clsval2  23207  opncldf1  23241  opncldf2  23242  opncldf3  23243  indiscld  23248  mretopd  23249  restcld  23329  lecldbas  23376  pnrmopn  23500  hauscmplem  23563  elpt  23729  elptr  23730  cfinfil  24050  csdfil  24051  ufilss  24062  filufint  24077  cfinufil  24085  ufinffr  24086  ufilen  24087  prdsxmslem2  24686  lebnumlem1  25120  bcth3  25490  ismbl  25685  ishpg  29041  plngval  29059  frgrwopregasn  30667  frgrwopregbsn  30668  disjdifprg  32920  0elsiga  34504  prsiga  34521  sigaclci  34522  difelsiga  34523  unelldsys  34548  sigapildsyslem  34551  sigapildsys  34552  ldgenpisyslem1  34553  isros  34558  unelros  34561  difelros  34562  inelsros  34568  diffiunisros  34569  rossros  34570  elcarsg  34695  ballotlemfval  34880  ballotlemgval  34914  kur14lem1  35698  topdifinffinlem  37993  topdifinffin  37994  oe0rif  44012  dssmapfv3d  44745  dssmapnvod  44746  clsk3nimkb  44766  ntrclsneine0lem  44790  ntrclsk2  44794  ntrclskb  44795  ntrclsk13  44797  ntrclsk4  44798  prsal  47032  saldifcl  47033  salexct  47048  salexct2  47053  salexct3  47056  salgencntex  47057  salgensscntex  47058  caragenel  47209  opncldeqv  49680