Theorem difeq1 4070

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ∈ wcel 2109  {crab 3394   ∖ cdif 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-dif 3906

This theorem is referenced by:  difeq12  4072  difeq1i  4073  difeq1d  4076  symdifeq1  4206  uneqdifeq  4444  hartogslem1  9434  kmlem9  10053  kmlem11  10055  kmlem12  10056  isfin1a  10186  fin1a2lem13  10306  fundmge2nop0  14409  incexclem  15743  coprmprod  16572  coprmproddvds  16574  ismri  17537  f1otrspeq  19326  pmtrval  19330  pmtrfrn  19337  symgsssg  19346  symgfisg  19347  symggen  19349  psgnunilem1  19372  psgnunilem5  19373  psgneldm  19382  ablfac1eulem  19953  sdrgacs  20686  islbs  20980  lbsextlem1  21065  lbsextlem2  21066  lbsextlem3  21067  lbsextlem4  21068  cofipsgn  21500  selvffval  22018  submafval  22464  m1detdiag  22482  lpval  23024  2ndcdisj  23341  isufil  23788  ptcmplem2  23938  mblsplit  25431  voliunlem3  25451  ig1pval  26079  nbgr2vtx1edg  29295  nbuhgr2vtx1edgb  29297  nb3grprlem2  29326  uvtx01vtx  29342  cplgr1v  29375  dfconngr1  30132  isconngr1  30134  isfrgr  30204  frgr1v  30215  nfrgr2v  30216  frgr3v  30219  1vwmgr  30220  3vfriswmgr  30222  difeq  32462  symgcntz  33027  tocycval  33050  sigaval  34078  issiga  34079  issgon  34090  isros  34135  unelros  34138  difelros  34139  inelsros  34145  diffiunisros  34146  rossros  34147  inelcarsg  34279  carsgclctunlem2  34287  probun  34387  ballotlemgval  34492  cvmscbv  35231  cvmsi  35238  cvmsval  35239  poimirlem4  37604  dssmapfvd  43990  compne  44414  dvmptfprod  45926  caragensplit  46481  vonvolmbllem  46641  vonvolmbl  46642  ldepsnlinc  48493  eenglngeehlnm  48724