Theorem difeq1 4078

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

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

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 3403  df-dif 3914

This theorem is referenced by:  difeq12  4080  difeq1i  4081  difeq1d  4084  symdifeq1  4214  uneqdifeq  4452  hartogslem1  9471  kmlem9  10088  kmlem11  10090  kmlem12  10091  isfin1a  10221  fin1a2lem13  10341  fundmge2nop0  14443  incexclem  15778  coprmprod  16607  coprmproddvds  16609  ismri  17568  f1otrspeq  19353  pmtrval  19357  pmtrfrn  19364  symgsssg  19373  symgfisg  19374  symggen  19376  psgnunilem1  19399  psgnunilem5  19400  psgneldm  19409  ablfac1eulem  19980  sdrgacs  20686  islbs  20959  lbsextlem1  21044  lbsextlem2  21045  lbsextlem3  21046  lbsextlem4  21047  cofipsgn  21478  selvffval  21996  submafval  22442  m1detdiag  22460  lpval  23002  2ndcdisj  23319  isufil  23766  ptcmplem2  23916  mblsplit  25409  voliunlem3  25429  ig1pval  26057  nbgr2vtx1edg  29253  nbuhgr2vtx1edgb  29255  nb3grprlem2  29284  uvtx01vtx  29300  cplgr1v  29333  dfconngr1  30090  isconngr1  30092  isfrgr  30162  frgr1v  30173  nfrgr2v  30174  frgr3v  30177  1vwmgr  30178  3vfriswmgr  30180  difeq  32420  symgcntz  33015  tocycval  33038  sigaval  34074  issiga  34075  issgon  34086  isros  34131  unelros  34134  difelros  34135  inelsros  34141  diffiunisros  34142  rossros  34143  inelcarsg  34275  carsgclctunlem2  34283  probun  34383  ballotlemgval  34488  cvmscbv  35218  cvmsi  35225  cvmsval  35226  poimirlem4  37591  dssmapfvd  43979  compne  44403  dvmptfprod  45916  caragensplit  46471  vonvolmbllem  46631  vonvolmbl  46632  ldepsnlinc  48470  eenglngeehlnm  48701