Theorem difeq1 4073

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 3415	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐶} = {𝑥 ∈ 𝐵 ∣ ¬ 𝑥 ∈ 𝐶})
2		dfdif2 3912	. 2 ⊢ (𝐴 ∖ 𝐶) = {𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝐶}
3		dfdif2 3912	. 2 ⊢ (𝐵 ∖ 𝐶) = {𝑥 ∈ 𝐵 ∣ ¬ 𝑥 ∈ 𝐶}
4	1, 2, 3	3eqtr4g 2797	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ∈ wcel 2114  {crab 3401   ∖ cdif 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-dif 3906

This theorem is referenced by:  difeq12  4075  difeq1i  4076  difeq1d  4079  symdifeq1  4209  uneqdifeq  4447  hartogslem1  9459  kmlem9  10081  kmlem11  10083  kmlem12  10084  isfin1a  10214  fin1a2lem13  10334  fundmge2nop0  14437  incexclem  15771  coprmprod  16600  coprmproddvds  16602  ismri  17566  f1otrspeq  19388  pmtrval  19392  pmtrfrn  19399  symgsssg  19408  symgfisg  19409  symggen  19411  psgnunilem1  19434  psgnunilem5  19435  psgneldm  19444  ablfac1eulem  20015  sdrgacs  20746  islbs  21040  lbsextlem1  21125  lbsextlem2  21126  lbsextlem3  21127  lbsextlem4  21128  cofipsgn  21560  selvffval  22088  submafval  22535  m1detdiag  22553  lpval  23095  2ndcdisj  23412  isufil  23859  ptcmplem2  24009  mblsplit  25501  voliunlem3  25521  ig1pval  26149  nbgr2vtx1edg  29435  nbuhgr2vtx1edgb  29437  nb3grprlem2  29466  uvtx01vtx  29482  cplgr1v  29515  dfconngr1  30275  isconngr1  30277  isfrgr  30347  frgr1v  30358  nfrgr2v  30359  frgr3v  30362  1vwmgr  30363  3vfriswmgr  30365  difeq  32605  symgcntz  33179  tocycval  33202  extvval  33708  sigaval  34289  issiga  34290  issgon  34301  isros  34346  unelros  34349  difelros  34350  inelsros  34356  diffiunisros  34357  rossros  34358  inelcarsg  34489  carsgclctunlem2  34497  probun  34597  ballotlemgval  34702  cvmscbv  35474  cvmsi  35481  cvmsval  35482  poimirlem4  37875  dssmapfvd  44373  compne  44796  dvmptfprod  46303  caragensplit  46858  vonvolmbllem  47018  vonvolmbl  47019  ldepsnlinc  48868  eenglngeehlnm  49099