Theorem difeq1 4094

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ∈ wcel 2114  {crab 3144   ∖ cdif 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-rab 3149  df-dif 3941

This theorem is referenced by:  difeq12  4096  difeq1i  4097  difeq1d  4100  symdifeq1  4223  uneqdifeq  4440  hartogslem1  9008  kmlem9  9586  kmlem11  9588  kmlem12  9589  isfin1a  9716  fin1a2lem13  9836  fundmge2nop0  13853  incexclem  15193  coprmprod  16007  coprmproddvds  16009  ismri  16904  f1otrspeq  18577  pmtrval  18581  pmtrfrn  18588  symgsssg  18597  symgfisg  18598  symggen  18600  psgnunilem1  18623  psgnunilem5  18624  psgneldm  18633  ablfac1eulem  19196  sdrgacs  19582  islbs  19850  lbsextlem1  19932  lbsextlem2  19933  lbsextlem3  19934  lbsextlem4  19935  selvffval  20331  cofipsgn  20739  submafval  21190  m1detdiag  21208  lpval  21749  2ndcdisj  22066  isufil  22513  ptcmplem2  22663  mblsplit  24135  voliunlem3  24155  ig1pval  24768  nbgr2vtx1edg  27134  nbuhgr2vtx1edgb  27136  nbgr0vtx  27140  nb3grprlem2  27165  uvtx01vtx  27181  cplgr1v  27214  dfconngr1  27969  isconngr1  27971  isfrgr  28041  frgr1v  28052  nfrgr2v  28053  frgr3v  28056  1vwmgr  28057  3vfriswmgr  28059  difeq  30282  symgcntz  30731  tocycval  30752  sigaval  31372  issiga  31373  issgon  31384  isros  31429  unelros  31432  difelros  31433  inelsros  31439  diffiunisros  31440  rossros  31441  inelcarsg  31571  carsgclctunlem2  31579  probun  31679  ballotlemgval  31783  cvmscbv  32507  cvmsi  32514  cvmsval  32515  poimirlem4  34898  dssmapfvd  40370  compne  40780  dvmptfprod  42237  caragensplit  42789  vonvolmbllem  42949  vonvolmbl  42950  ldepsnlinc  44570  eenglngeehlnm  44733