Theorem difeq1 4067

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2145  {crab 3413   ∖ 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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-dif 3902

This theorem is used by:  difeq12  4069  difeq1i  4070  difeq1d  4073  symdifeq1  4201  uneqdifeq  4448  hartogslem1  9529  kmlem9  10230  kmlem11  10232  kmlem12  10233  isfin1a  10363  fin1a2lem13  10483  fundmge2nop0  14640  incexclem  15998  coprmprod  16829  coprmproddvds  16831  ismri  17798  f1otrspeq  19654  pmtrval  19658  pmtrfrn  19665  symgsssg  19674  symgfisg  19675  symggen  19677  psgnunilem1  19700  psgnunilem5  19701  psgneldm  19710  ablfac1eulem  20281  sdrgacs  21051  islbs  21344  lbsextlem1  21429  lbsextlem2  21430  lbsextlem3  21431  lbsextlem4  21432  cofipsgn  21892  selvffval  22420  submafval  22887  m1detdiag  22905  lpval  23450  2ndcdisj  23768  isufil  24215  ptcmplem2  24365  mblsplit  25846  voliunlem3  25866  ig1pval  26487  nbgr2vtx1edg  29924  nbuhgr2vtx1edgb  29926  nb3grprlem2  29955  uvtx01vtx  29971  cplgr1v  30004  dfconngr1  30782  isconngr1  30784  isfrgr  30854  frgr1v  30865  nfrgr2v  30866  frgr3v  30869  1vwmgr  30870  3vfriswmgr  30872  difeq  33107  symgcntz  33639  tocycval  33662  extvval  34156  sigaval  34736  issiga  34737  issgon  34748  isros  34794  unelros  34797  difelros  34798  inelsros  34804  diffiunisros  34805  rossros  34806  inelcarsg  34936  carsgclctunlem2  34944  probun  35044  ballotlemgval  35149  cvmscbv  36002  cvmsi  36009  cvmsval  36010  poimirlem4  38522  dssmapfvd  45002  compne  45409  dvmptfprod  46924  caragensplit  47479  vonvolmbllem  47639  vonvolmbl  47640  ldepsnlinc  49589  eenglngeehlnm  49820