Theorem difeq1 4128

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1536   ∈ wcel 2105  {crab 3432   ∖ cdif 3959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-dif 3965

This theorem is referenced by:  difeq12  4130  difeq1i  4131  difeq1d  4134  symdifeq1  4260  uneqdifeq  4498  hartogslem1  9579  kmlem9  10196  kmlem11  10198  kmlem12  10199  isfin1a  10329  fin1a2lem13  10449  fundmge2nop0  14537  incexclem  15868  coprmprod  16694  coprmproddvds  16696  ismri  17675  f1otrspeq  19479  pmtrval  19483  pmtrfrn  19490  symgsssg  19499  symgfisg  19500  symggen  19502  psgnunilem1  19525  psgnunilem5  19526  psgneldm  19535  ablfac1eulem  20106  sdrgacs  20818  islbs  21092  lbsextlem1  21177  lbsextlem2  21178  lbsextlem3  21179  lbsextlem4  21180  cofipsgn  21628  selvffval  22154  submafval  22600  m1detdiag  22618  lpval  23162  2ndcdisj  23479  isufil  23926  ptcmplem2  24076  mblsplit  25580  voliunlem3  25600  ig1pval  26229  nbgr2vtx1edg  29381  nbuhgr2vtx1edgb  29383  nb3grprlem2  29412  uvtx01vtx  29428  cplgr1v  29461  dfconngr1  30216  isconngr1  30218  isfrgr  30288  frgr1v  30299  nfrgr2v  30300  frgr3v  30303  1vwmgr  30304  3vfriswmgr  30306  difeq  32545  symgcntz  33087  tocycval  33110  sigaval  34091  issiga  34092  issgon  34103  isros  34148  unelros  34151  difelros  34152  inelsros  34158  diffiunisros  34159  rossros  34160  inelcarsg  34292  carsgclctunlem2  34300  probun  34400  ballotlemgval  34504  cvmscbv  35242  cvmsi  35249  cvmsval  35250  poimirlem4  37610  dssmapfvd  44006  compne  44436  dvmptfprod  45900  caragensplit  46455  vonvolmbllem  46615  vonvolmbl  46616  ldepsnlinc  48353  eenglngeehlnm  48588