Theorem difeq1 4050

Description: Equality theorem for class difference. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

Ref	Expression
difeq1	⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))

Proof of Theorem difeq1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rabeq 3418	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐶} = {𝑥 ∈ 𝐵 ∣ ¬ 𝑥 ∈ 𝐶})
2		dfdif2 3896	. 2 ⊢ (𝐴 ∖ 𝐶) = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐶}
3		dfdif2 3896	. 2 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∈ 𝐵 ∣ ¬ 𝑥 ∈ 𝐶}
4	1, 2, 3	3eqtr4g 2803	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ∈ wcel 2106  {crab 3068   ∖ cdif 3884

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-dif 3890

This theorem is referenced by:  difeq12  4052  difeq1i  4053  difeq1d  4056  symdifeq1  4178  uneqdifeq  4423  hartogslem1  9301  kmlem9  9914  kmlem11  9916  kmlem12  9917  isfin1a  10048  fin1a2lem13  10168  fundmge2nop0  14206  incexclem  15548  coprmprod  16366  coprmproddvds  16368  ismri  17340  f1otrspeq  19055  pmtrval  19059  pmtrfrn  19066  symgsssg  19075  symgfisg  19076  symggen  19078  psgnunilem1  19101  psgnunilem5  19102  psgneldm  19111  ablfac1eulem  19675  sdrgacs  20069  islbs  20338  lbsextlem1  20420  lbsextlem2  20421  lbsextlem3  20422  lbsextlem4  20423  cofipsgn  20798  selvffval  21326  submafval  21728  m1detdiag  21746  lpval  22290  2ndcdisj  22607  isufil  23054  ptcmplem2  23204  mblsplit  24696  voliunlem3  24716  ig1pval  25337  nbgr2vtx1edg  27717  nbuhgr2vtx1edgb  27719  nbgr0vtx  27723  nb3grprlem2  27748  uvtx01vtx  27764  cplgr1v  27797  dfconngr1  28552  isconngr1  28554  isfrgr  28624  frgr1v  28635  nfrgr2v  28636  frgr3v  28639  1vwmgr  28640  3vfriswmgr  28642  difeq  30865  symgcntz  31354  tocycval  31375  sigaval  32079  issiga  32080  issgon  32091  isros  32136  unelros  32139  difelros  32140  inelsros  32146  diffiunisros  32147  rossros  32148  inelcarsg  32278  carsgclctunlem2  32286  probun  32386  ballotlemgval  32490  cvmscbv  33220  cvmsi  33227  cvmsval  33228  poimirlem4  35781  dssmapfvd  41625  compne  42059  dvmptfprod  43486  caragensplit  44038  vonvolmbllem  44198  vonvolmbl  44199  ldepsnlinc  45849  eenglngeehlnm  46085