Theorem difeq2 4117

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ∈ wcel 2107  {crab 3433   ∖ cdif 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-dif 3952

This theorem is referenced by:  difeq12  4118  difeq2i  4120  difeq2d  4123  symdifeq1  4245  ssdifim  4263  disjdif2  4480  ssdifeq0  4487  sorpsscmpl  7724  2oconcl  8503  oev  8514  sbthlem2  9084  sbth  9093  sbthfi  9202  infdiffi  9653  fin1ai  10288  fin23lem7  10311  fin23lem11  10312  compsscnv  10366  isf34lem1  10367  compss  10371  isf34lem4  10372  fin1a2lem7  10401  pwfseqlem4a  10656  pwfseqlem4  10657  efgmval  19580  efgi  19587  frgpuptinv  19639  gsumcllem  19776  gsumzaddlem  19789  selvfval  21680  fctop  22507  cctop  22509  iscld  22531  clsval2  22554  opncldf1  22588  opncldf2  22589  opncldf3  22590  indiscld  22595  mretopd  22596  restcld  22676  lecldbas  22723  pnrmopn  22847  hauscmplem  22910  elpt  23076  elptr  23077  cfinfil  23397  csdfil  23398  ufilss  23409  filufint  23424  cfinufil  23432  ufinffr  23433  ufilen  23434  prdsxmslem2  24038  lebnumlem1  24477  bcth3  24848  ismbl  25043  ishpg  28010  frgrwopregasn  29569  frgrwopregbsn  29570  disjdifprg  31806  0elsiga  33112  prsiga  33129  sigaclci  33130  difelsiga  33131  unelldsys  33156  sigapildsyslem  33159  sigapildsys  33160  ldgenpisyslem1  33161  isros  33166  unelros  33169  difelros  33170  inelsros  33176  diffiunisros  33177  rossros  33178  elcarsg  33304  ballotlemfval  33488  ballotlemgval  33522  kur14lem1  34197  topdifinffinlem  36228  topdifinffin  36229  oe0rif  42035  dssmapfv3d  42770  dssmapnvod  42771  clsk3nimkb  42791  ntrclsneine0lem  42815  ntrclsk2  42819  ntrclskb  42820  ntrclsk13  42822  ntrclsk4  42823  prsal  45034  saldifcl  45035  salexct  45050  salexct2  45055  salexct3  45058  salgencntex  45059  salgensscntex  45060  caragenel  45211  opncldeqv  47534