Theorem difeq2 4060

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2147  {crab 3416   ∖ cdif 4048

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-dif 4050

This theorem is used by:  difeq12  4061  difeq2i  4063  difeq2d  4066  symdifeq1  4203  ssdifim  4221  disjdif2  4439  ssdifeq0  4445  xpdifcnvepel  6178  sorpsscmpl  7782  2oconcl  8549  oev  8560  sbthlem2  9145  sbth  9154  sbthfi  9252  infdiffi  9696  fin1ai  10410  fin23lem7  10433  fin23lem11  10434  compsscnv  10488  isf34lem1  10489  compss  10493  isf34lem4  10494  fin1a2lem7  10523  pwfseqlem4a  10785  pwfseqlem4  10786  efgmval  19977  efgi  19984  frgpuptinv  20036  gsumcllem  20173  gsumzaddlem  20186  selvfval  22483  fctop  23377  cctop  23379  iscld  23400  clsval2  23423  opncldf1  23457  opncldf2  23458  opncldf3  23459  indiscld  23464  mretopd  23465  restcld  23545  lecldbas  23592  pnrmopn  23716  hauscmplem  23779  elpt  23946  elptr  23947  cfinfil  24267  csdfil  24268  ufilss  24279  filufint  24294  cfinufil  24302  ufinffr  24303  ufilen  24304  prdsxmslem2  24903  lebnumlem1  25337  bcth3  25707  ismbl  25902  ishpg  29294  plngval  29312  frgrwopregasn  30974  frgrwopregbsn  30975  disjdifprg  33267  0elsiga  34857  prsiga  34874  sigaclci  34875  difunielsiga  34876  unelldsys  34902  sigapildsyslem  34905  sigapildsys  34906  ldgenpisyslem1  34907  isros  34912  unelros  34915  difelros  34916  inelsros  34922  diffiunisros  34923  rossros  34924  elcarsg  35048  ballotlemfval  35233  ballotlemgval  35267  gdlop3fv  36006  kur14lem1  36179  topdifinffinlem  38538  topdifinffin  38539  oe0rif  44548  dssmapfv3d  45280  dssmapnvod  45281  clsk3nimkb  45301  ntrclsneine0lem  45325  ntrclsk2  45329  ntrclskb  45330  ntrclsk13  45332  ntrclsk4  45333  prsal  47601  saldifcl  47602  salexct  47617  salexct2  47622  salexct3  47625  salgencntex  47626  salgensscntex  47627  caragenel  47778  opncldbid  50347