Theorem difeq1 4071

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1559   ∈ wcel 2141  {crab 3413   ∖ cdif 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-dif 3905

This theorem is referenced by:  difeq12  4073  difeq1i  4074  difeq1d  4077  symdifeq1  4205  uneqdifeq  4443  hartogslem1  9484  kmlem9  10109  kmlem11  10111  kmlem12  10112  isfin1a  10243  fin1a2lem13  10363  fundmge2nop0  14509  incexclem  15857  coprmprod  16686  coprmproddvds  16688  ismri  17654  f1otrspeq  19478  pmtrval  19482  pmtrfrn  19489  symgsssg  19498  symgfisg  19499  symggen  19501  psgnunilem1  19524  psgnunilem5  19525  psgneldm  19534  ablfac1eulem  20105  sdrgacs  20838  islbs  21131  lbsextlem1  21216  lbsextlem2  21217  lbsextlem3  21218  lbsextlem4  21219  cofipsgn  21633  selvffval  22159  submafval  22627  m1detdiag  22645  lpval  23187  2ndcdisj  23504  isufil  23951  ptcmplem2  24101  mblsplit  25582  voliunlem3  25602  ig1pval  26224  nbgr2vtx1edg  29508  nbuhgr2vtx1edgb  29510  nb3grprlem2  29539  uvtx01vtx  29555  cplgr1v  29588  dfconngr1  30347  isconngr1  30349  isfrgr  30419  frgr1v  30430  nfrgr2v  30431  frgr3v  30434  1vwmgr  30435  3vfriswmgr  30437  difeq  32677  symgcntz  33226  tocycval  33249  extvval  33789  sigaval  34369  issiga  34370  issgon  34381  isros  34426  unelros  34429  difelros  34430  inelsros  34436  diffiunisros  34437  rossros  34438  inelcarsg  34569  carsgclctunlem2  34577  probun  34677  ballotlemgval  34782  cvmscbv  35569  cvmsi  35576  cvmsval  35577  poimirlem4  38084  dssmapfvd  44554  compne  44977  dvmptfprod  46480  caragensplit  47035  vonvolmbllem  47195  vonvolmbl  47196  ldepsnlinc  49091  eenglngeehlnm  49322