Theorem difeq1 4059

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-dif 3892

This theorem is referenced by:  difeq12  4061  difeq1i  4062  difeq1d  4065  symdifeq1  4195  uneqdifeq  4432  hartogslem1  9457  kmlem9  10081  kmlem11  10083  kmlem12  10084  isfin1a  10214  fin1a2lem13  10334  fundmge2nop0  14464  incexclem  15801  coprmprod  16630  coprmproddvds  16632  ismri  17597  f1otrspeq  19422  pmtrval  19426  pmtrfrn  19433  symgsssg  19442  symgfisg  19443  symggen  19445  psgnunilem1  19468  psgnunilem5  19469  psgneldm  19478  ablfac1eulem  20049  sdrgacs  20778  islbs  21071  lbsextlem1  21156  lbsextlem2  21157  lbsextlem3  21158  lbsextlem4  21159  cofipsgn  21573  selvffval  22099  submafval  22544  m1detdiag  22562  lpval  23104  2ndcdisj  23421  isufil  23868  ptcmplem2  24018  mblsplit  25499  voliunlem3  25519  ig1pval  26141  nbgr2vtx1edg  29419  nbuhgr2vtx1edgb  29421  nb3grprlem2  29450  uvtx01vtx  29466  cplgr1v  29499  dfconngr1  30258  isconngr1  30260  isfrgr  30330  frgr1v  30341  nfrgr2v  30342  frgr3v  30345  1vwmgr  30346  3vfriswmgr  30348  difeq  32588  symgcntz  33146  tocycval  33169  extvval  33675  sigaval  34255  issiga  34256  issgon  34267  isros  34312  unelros  34315  difelros  34316  inelsros  34322  diffiunisros  34323  rossros  34324  inelcarsg  34455  carsgclctunlem2  34463  probun  34563  ballotlemgval  34668  cvmscbv  35440  cvmsi  35447  cvmsval  35448  poimirlem4  37945  dssmapfvd  44444  compne  44867  dvmptfprod  46373  caragensplit  46928  vonvolmbllem  47088  vonvolmbl  47089  ldepsnlinc  48984  eenglngeehlnm  49215