Theorem difeq2 4078

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2146  {crab 3419   ∖ cdif 3905

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-dif 3911

This theorem is used by:  difeq12  4079  difeq2i  4081  difeq2d  4084  symdifeq1  4211  ssdifim  4229  disjdif2  4446  ssdifeq0  4452  xpdifcnvepel  6171  sorpsscmpl  7744  2oconcl  8497  oev  8508  sbthlem2  9086  sbth  9095  sbthfi  9193  infdiffi  9637  fin1ai  10295  fin23lem7  10318  fin23lem11  10319  compsscnv  10373  isf34lem1  10374  compss  10378  isf34lem4  10379  fin1a2lem7  10408  pwfseqlem4a  10664  pwfseqlem4  10665  efgmval  19807  efgi  19814  frgpuptinv  19866  gsumcllem  20003  gsumzaddlem  20016  selvfval  22300  fctop  23191  cctop  23193  iscld  23214  clsval2  23237  opncldf1  23271  opncldf2  23272  opncldf3  23273  indiscld  23278  mretopd  23279  restcld  23359  lecldbas  23406  pnrmopn  23530  hauscmplem  23593  elpt  23759  elptr  23760  cfinfil  24080  csdfil  24081  ufilss  24092  filufint  24107  cfinufil  24115  ufinffr  24116  ufilen  24117  prdsxmslem2  24716  lebnumlem1  25150  bcth3  25520  ismbl  25715  ishpg  29071  plngval  29089  frgrwopregasn  30697  frgrwopregbsn  30698  disjdifprg  32950  0elsiga  34528  prsiga  34545  sigaclci  34546  difelsiga  34547  unelldsys  34572  sigapildsyslem  34575  sigapildsys  34576  ldgenpisyslem1  34577  isros  34582  unelros  34585  difelros  34586  inelsros  34592  diffiunisros  34593  rossros  34594  elcarsg  34719  ballotlemfval  34904  ballotlemgval  34938  kur14lem1  35711  topdifinffinlem  38026  topdifinffin  38027  oe0rif  44045  dssmapfv3d  44778  dssmapnvod  44779  clsk3nimkb  44799  ntrclsneine0lem  44823  ntrclsk2  44827  ntrclskb  44828  ntrclsk13  44830  ntrclsk4  44831  prsal  47065  saldifcl  47066  salexct  47081  salexct2  47086  salexct3  47089  salgencntex  47090  salgensscntex  47091  caragenel  47242  opncldeqv  49713