Theorem difeq1 4116

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ∈ wcel 2107  {crab 3433   ∖ cdif 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-dif 3952

This theorem is referenced by:  difeq12  4118  difeq1i  4119  difeq1d  4122  symdifeq1  4245  uneqdifeq  4493  hartogslem1  9537  kmlem9  10153  kmlem11  10155  kmlem12  10156  isfin1a  10287  fin1a2lem13  10407  fundmge2nop0  14453  incexclem  15782  coprmprod  16598  coprmproddvds  16600  ismri  17575  f1otrspeq  19315  pmtrval  19319  pmtrfrn  19326  symgsssg  19335  symgfisg  19336  symggen  19338  psgnunilem1  19361  psgnunilem5  19362  psgneldm  19371  ablfac1eulem  19942  sdrgacs  20417  islbs  20687  lbsextlem1  20771  lbsextlem2  20772  lbsextlem3  20773  lbsextlem4  20774  cofipsgn  21146  selvffval  21679  submafval  22081  m1detdiag  22099  lpval  22643  2ndcdisj  22960  isufil  23407  ptcmplem2  23557  mblsplit  25049  voliunlem3  25069  ig1pval  25690  nbgr2vtx1edg  28638  nbuhgr2vtx1edgb  28640  nbgr0vtx  28644  nb3grprlem2  28669  uvtx01vtx  28685  cplgr1v  28718  dfconngr1  29472  isconngr1  29474  isfrgr  29544  frgr1v  29555  nfrgr2v  29556  frgr3v  29559  1vwmgr  29560  3vfriswmgr  29562  difeq  31787  symgcntz  32277  tocycval  32298  sigaval  33140  issiga  33141  issgon  33152  isros  33197  unelros  33200  difelros  33201  inelsros  33207  diffiunisros  33208  rossros  33209  inelcarsg  33341  carsgclctunlem2  33349  probun  33449  ballotlemgval  33553  cvmscbv  34280  cvmsi  34287  cvmsval  34288  poimirlem4  36540  dssmapfvd  42816  compne  43248  dvmptfprod  44709  caragensplit  45264  vonvolmbllem  45424  vonvolmbl  45425  ldepsnlinc  47237  eenglngeehlnm  47473