Theorem difeq1 4085

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-dif 3920

This theorem is referenced by:  difeq12  4087  difeq1i  4088  difeq1d  4091  symdifeq1  4221  uneqdifeq  4459  hartogslem1  9502  kmlem9  10119  kmlem11  10121  kmlem12  10122  isfin1a  10252  fin1a2lem13  10372  fundmge2nop0  14474  incexclem  15809  coprmprod  16638  coprmproddvds  16640  ismri  17599  f1otrspeq  19384  pmtrval  19388  pmtrfrn  19395  symgsssg  19404  symgfisg  19405  symggen  19407  psgnunilem1  19430  psgnunilem5  19431  psgneldm  19440  ablfac1eulem  20011  sdrgacs  20717  islbs  20990  lbsextlem1  21075  lbsextlem2  21076  lbsextlem3  21077  lbsextlem4  21078  cofipsgn  21509  selvffval  22027  submafval  22473  m1detdiag  22491  lpval  23033  2ndcdisj  23350  isufil  23797  ptcmplem2  23947  mblsplit  25440  voliunlem3  25460  ig1pval  26088  nbgr2vtx1edg  29284  nbuhgr2vtx1edgb  29286  nb3grprlem2  29315  uvtx01vtx  29331  cplgr1v  29364  dfconngr1  30124  isconngr1  30126  isfrgr  30196  frgr1v  30207  nfrgr2v  30208  frgr3v  30211  1vwmgr  30212  3vfriswmgr  30214  difeq  32454  symgcntz  33049  tocycval  33072  sigaval  34108  issiga  34109  issgon  34120  isros  34165  unelros  34168  difelros  34169  inelsros  34175  diffiunisros  34176  rossros  34177  inelcarsg  34309  carsgclctunlem2  34317  probun  34417  ballotlemgval  34522  cvmscbv  35252  cvmsi  35259  cvmsval  35260  poimirlem4  37625  dssmapfvd  44013  compne  44437  dvmptfprod  45950  caragensplit  46505  vonvolmbllem  46665  vonvolmbl  46666  ldepsnlinc  48501  eenglngeehlnm  48732