Theorem difeq2 4116

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ∈ wcel 2105  {crab 3431   ∖ cdif 3945

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-dif 3951

This theorem is referenced by:  difeq12  4117  difeq2i  4119  difeq2d  4122  symdifeq1  4244  ssdifim  4262  disjdif2  4479  ssdifeq0  4486  sorpsscmpl  7728  2oconcl  8509  oev  8520  sbthlem2  9090  sbth  9099  sbthfi  9208  infdiffi  9659  fin1ai  10294  fin23lem7  10317  fin23lem11  10318  compsscnv  10372  isf34lem1  10373  compss  10377  isf34lem4  10378  fin1a2lem7  10407  pwfseqlem4a  10662  pwfseqlem4  10663  efgmval  19625  efgi  19632  frgpuptinv  19684  gsumcllem  19821  gsumzaddlem  19834  selvfval  21901  fctop  22740  cctop  22742  iscld  22764  clsval2  22787  opncldf1  22821  opncldf2  22822  opncldf3  22823  indiscld  22828  mretopd  22829  restcld  22909  lecldbas  22956  pnrmopn  23080  hauscmplem  23143  elpt  23309  elptr  23310  cfinfil  23630  csdfil  23631  ufilss  23642  filufint  23657  cfinufil  23665  ufinffr  23666  ufilen  23667  prdsxmslem2  24271  lebnumlem1  24720  bcth3  25092  ismbl  25288  ishpg  28292  frgrwopregasn  29851  frgrwopregbsn  29852  disjdifprg  32088  0elsiga  33425  prsiga  33442  sigaclci  33443  difelsiga  33444  unelldsys  33469  sigapildsyslem  33472  sigapildsys  33473  ldgenpisyslem1  33474  isros  33479  unelros  33482  difelros  33483  inelsros  33489  diffiunisros  33490  rossros  33491  elcarsg  33617  ballotlemfval  33801  ballotlemgval  33835  kur14lem1  34510  topdifinffinlem  36544  topdifinffin  36545  oe0rif  42350  dssmapfv3d  43085  dssmapnvod  43086  clsk3nimkb  43106  ntrclsneine0lem  43130  ntrclsk2  43134  ntrclskb  43135  ntrclsk13  43137  ntrclsk4  43138  prsal  45345  saldifcl  45346  salexct  45361  salexct2  45366  salexct3  45369  salgencntex  45370  salgensscntex  45371  caragenel  45522  opncldeqv  47634