Theorem difeq2 4068

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2145  {crab 3412   ∖ cdif 3896

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-dif 3902

This theorem is used by:  difeq12  4069  difeq2i  4071  difeq2d  4074  symdifeq1  4201  ssdifim  4219  disjdif2  4436  ssdifeq0  4442  xpdifcnvepel  6161  sorpsscmpl  7736  2oconcl  8491  oev  8502  sbthlem2  9087  sbth  9096  sbthfi  9194  infdiffi  9638  fin1ai  10296  fin23lem7  10319  fin23lem11  10320  compsscnv  10374  isf34lem1  10375  compss  10379  isf34lem4  10380  fin1a2lem7  10409  pwfseqlem4a  10671  pwfseqlem4  10672  efgmval  19840  efgi  19847  frgpuptinv  19899  gsumcllem  20036  gsumzaddlem  20049  selvfval  22336  fctop  23230  cctop  23232  iscld  23253  clsval2  23276  opncldf1  23310  opncldf2  23311  opncldf3  23312  indiscld  23317  mretopd  23318  restcld  23398  lecldbas  23445  pnrmopn  23569  hauscmplem  23632  elpt  23799  elptr  23800  cfinfil  24120  csdfil  24121  ufilss  24132  filufint  24147  cfinufil  24155  ufinffr  24156  ufilen  24157  prdsxmslem2  24756  lebnumlem1  25190  bcth3  25560  ismbl  25755  ishpg  29117  plngval  29135  frgrwopregasn  30797  frgrwopregbsn  30798  disjdifprg  33049  0elsiga  34625  prsiga  34642  sigaclci  34643  difunielsiga  34644  unelldsys  34670  sigapildsyslem  34673  sigapildsys  34674  ldgenpisyslem1  34675  isros  34680  unelros  34683  difelros  34684  inelsros  34690  diffiunisros  34691  rossros  34692  elcarsg  34817  ballotlemfval  35002  ballotlemgval  35036  kur14lem1  35786  topdifinffinlem  38102  topdifinffin  38103  oe0rif  44127  dssmapfv3d  44860  dssmapnvod  44861  clsk3nimkb  44881  ntrclsneine0lem  44905  ntrclsk2  44909  ntrclskb  44910  ntrclsk13  44912  ntrclsk4  44913  prsal  47147  saldifcl  47148  salexct  47163  salexct2  47168  salexct3  47171  salgencntex  47172  salgensscntex  47173  caragenel  47324  opncldeqv  49829