Theorem difeq1 4043

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   ∈ wcel 2111  {crab 3110   ∖ cdif 3878

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-dif 3884

This theorem is referenced by:  difeq12  4045  difeq1i  4046  difeq1d  4049  symdifeq1  4171  uneqdifeq  4396  hartogslem1  8990  kmlem9  9569  kmlem11  9571  kmlem12  9572  isfin1a  9703  fin1a2lem13  9823  fundmge2nop0  13846  incexclem  15183  coprmprod  15995  coprmproddvds  15997  ismri  16894  f1otrspeq  18567  pmtrval  18571  pmtrfrn  18578  symgsssg  18587  symgfisg  18588  symggen  18590  psgnunilem1  18613  psgnunilem5  18614  psgneldm  18623  ablfac1eulem  19187  sdrgacs  19573  islbs  19841  lbsextlem1  19923  lbsextlem2  19924  lbsextlem3  19925  lbsextlem4  19926  cofipsgn  20282  selvffval  20788  submafval  21184  m1detdiag  21202  lpval  21744  2ndcdisj  22061  isufil  22508  ptcmplem2  22658  mblsplit  24136  voliunlem3  24156  ig1pval  24773  nbgr2vtx1edg  27140  nbuhgr2vtx1edgb  27142  nbgr0vtx  27146  nb3grprlem2  27171  uvtx01vtx  27187  cplgr1v  27220  dfconngr1  27973  isconngr1  27975  isfrgr  28045  frgr1v  28056  nfrgr2v  28057  frgr3v  28060  1vwmgr  28061  3vfriswmgr  28063  difeq  30289  symgcntz  30779  tocycval  30800  sigaval  31480  issiga  31481  issgon  31492  isros  31537  unelros  31540  difelros  31541  inelsros  31547  diffiunisros  31548  rossros  31549  inelcarsg  31679  carsgclctunlem2  31687  probun  31787  ballotlemgval  31891  cvmscbv  32618  cvmsi  32625  cvmsval  32626  poimirlem4  35061  dssmapfvd  40718  compne  41145  dvmptfprod  42587  caragensplit  43139  vonvolmbllem  43299  vonvolmbl  43300  ldepsnlinc  44917  eenglngeehlnm  45153