Theorem difeq1 4067

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2145  {crab 3413   ∖ cdif 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-dif 3902

This theorem is used by:  difeq12  4069  difeq1i  4070  difeq1d  4073  symdifeq1  4201  uneqdifeq  4448  hartogslem1  9536  kmlem9  10237  kmlem11  10239  kmlem12  10240  isfin1a  10370  fin1a2lem13  10490  fundmge2nop0  14647  incexclem  16005  coprmprod  16836  coprmproddvds  16838  ismri  17805  f1otrspeq  19661  pmtrval  19665  pmtrfrn  19672  symgsssg  19681  symgfisg  19682  symggen  19684  psgnunilem1  19707  psgnunilem5  19708  psgneldm  19717  ablfac1eulem  20288  sdrgacs  21058  islbs  21351  lbsextlem1  21436  lbsextlem2  21437  lbsextlem3  21438  lbsextlem4  21439  cofipsgn  21899  selvffval  22427  submafval  22894  m1detdiag  22912  lpval  23457  2ndcdisj  23775  isufil  24222  ptcmplem2  24372  mblsplit  25853  voliunlem3  25873  ig1pval  26494  nbgr2vtx1edg  29931  nbuhgr2vtx1edgb  29933  nb3grprlem2  29962  uvtx01vtx  29978  cplgr1v  30011  dfconngr1  30789  isconngr1  30791  isfrgr  30861  frgr1v  30872  nfrgr2v  30873  frgr3v  30876  1vwmgr  30877  3vfriswmgr  30879  difeq  33114  symgcntz  33646  tocycval  33669  extvval  34163  sigaval  34743  issiga  34744  issgon  34755  isros  34801  unelros  34804  difelros  34805  inelsros  34811  diffiunisros  34812  rossros  34813  inelcarsg  34943  carsgclctunlem2  34951  probun  35051  ballotlemgval  35156  cvmscbv  36023  cvmsi  36030  cvmsval  36031  poimirlem4  38542  dssmapfvd  45016  compne  45423  dvmptfprod  46954  caragensplit  47509  vonvolmbllem  47669  vonvolmbl  47670  ldepsnlinc  49619  eenglngeehlnm  49850