Theorem difeq1 4082

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

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

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 3406  df-dif 3917

This theorem is referenced by:  difeq12  4084  difeq1i  4085  difeq1d  4088  symdifeq1  4218  uneqdifeq  4456  hartogslem1  9495  kmlem9  10112  kmlem11  10114  kmlem12  10115  isfin1a  10245  fin1a2lem13  10365  fundmge2nop0  14467  incexclem  15802  coprmprod  16631  coprmproddvds  16633  ismri  17592  f1otrspeq  19377  pmtrval  19381  pmtrfrn  19388  symgsssg  19397  symgfisg  19398  symggen  19400  psgnunilem1  19423  psgnunilem5  19424  psgneldm  19433  ablfac1eulem  20004  sdrgacs  20710  islbs  20983  lbsextlem1  21068  lbsextlem2  21069  lbsextlem3  21070  lbsextlem4  21071  cofipsgn  21502  selvffval  22020  submafval  22466  m1detdiag  22484  lpval  23026  2ndcdisj  23343  isufil  23790  ptcmplem2  23940  mblsplit  25433  voliunlem3  25453  ig1pval  26081  nbgr2vtx1edg  29277  nbuhgr2vtx1edgb  29279  nb3grprlem2  29308  uvtx01vtx  29324  cplgr1v  29357  dfconngr1  30117  isconngr1  30119  isfrgr  30189  frgr1v  30200  nfrgr2v  30201  frgr3v  30204  1vwmgr  30205  3vfriswmgr  30207  difeq  32447  symgcntz  33042  tocycval  33065  sigaval  34101  issiga  34102  issgon  34113  isros  34158  unelros  34161  difelros  34162  inelsros  34168  diffiunisros  34169  rossros  34170  inelcarsg  34302  carsgclctunlem2  34310  probun  34410  ballotlemgval  34515  cvmscbv  35245  cvmsi  35252  cvmsval  35253  poimirlem4  37618  dssmapfvd  44006  compne  44430  dvmptfprod  45943  caragensplit  46498  vonvolmbllem  46658  vonvolmbl  46659  ldepsnlinc  48497  eenglngeehlnm  48728