Theorem difeq1 4073

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ∈ wcel 2114  {crab 3401   ∖ cdif 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-dif 3906

This theorem is referenced by:  difeq12  4075  difeq1i  4076  difeq1d  4079  symdifeq1  4209  uneqdifeq  4447  hartogslem1  9461  kmlem9  10083  kmlem11  10085  kmlem12  10086  isfin1a  10216  fin1a2lem13  10336  fundmge2nop0  14439  incexclem  15773  coprmprod  16602  coprmproddvds  16604  ismri  17568  f1otrspeq  19393  pmtrval  19397  pmtrfrn  19404  symgsssg  19413  symgfisg  19414  symggen  19416  psgnunilem1  19439  psgnunilem5  19440  psgneldm  19449  ablfac1eulem  20020  sdrgacs  20751  islbs  21045  lbsextlem1  21130  lbsextlem2  21131  lbsextlem3  21132  lbsextlem4  21133  cofipsgn  21565  selvffval  22093  submafval  22540  m1detdiag  22558  lpval  23100  2ndcdisj  23417  isufil  23864  ptcmplem2  24014  mblsplit  25506  voliunlem3  25526  ig1pval  26154  nbgr2vtx1edg  29441  nbuhgr2vtx1edgb  29443  nb3grprlem2  29472  uvtx01vtx  29488  cplgr1v  29521  dfconngr1  30281  isconngr1  30283  isfrgr  30353  frgr1v  30364  nfrgr2v  30365  frgr3v  30368  1vwmgr  30369  3vfriswmgr  30371  difeq  32611  symgcntz  33185  tocycval  33208  extvval  33714  sigaval  34295  issiga  34296  issgon  34307  isros  34352  unelros  34355  difelros  34356  inelsros  34362  diffiunisros  34363  rossros  34364  inelcarsg  34495  carsgclctunlem2  34503  probun  34603  ballotlemgval  34708  cvmscbv  35480  cvmsi  35487  cvmsval  35488  poimirlem4  37904  dssmapfvd  44402  compne  44825  dvmptfprod  46332  caragensplit  46887  vonvolmbllem  47047  vonvolmbl  47048  ldepsnlinc  48897  eenglngeehlnm  49128