Theorem difeq1 4055

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1569   ∈ wcel 2144  {crab 3412   ∖ cdif 4044

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-dif 4046

This theorem is used by:  difeq12  4057  difeq1i  4058  difeq1d  4061  symdifeq1  4199  uneqdifeq  4447  hartogslem1  9541  kmlem9  10242  kmlem11  10244  kmlem12  10245  isfin1a  10375  fin1a2lem13  10495  fundmge2nop0  14652  incexclem  16012  coprmprod  16843  coprmproddvds  16845  ismri  17812  f1otrspeq  19668  pmtrval  19672  pmtrfrn  19679  symgsssg  19688  symgfisg  19689  symggen  19691  psgnunilem1  19714  psgnunilem5  19715  psgneldm  19724  ablfac1eulem  20295  sdrgacs  21065  islbs  21358  lbsextlem1  21443  lbsextlem2  21444  lbsextlem3  21445  lbsextlem4  21446  cofipsgn  21906  selvffval  22434  submafval  22901  m1detdiag  22919  lpval  23464  2ndcdisj  23782  isufil  24229  ptcmplem2  24379  mblsplit  25860  voliunlem3  25880  ig1pval  26501  nbgr2vtx1edg  29938  nbuhgr2vtx1edgb  29940  nb3grprlem2  29969  uvtx01vtx  29985  cplgr1v  30018  dfconngr1  30796  isconngr1  30798  isfrgr  30868  frgr1v  30879  nfrgr2v  30880  frgr3v  30883  1vwmgr  30884  3vfriswmgr  30886  difeq  33163  symgcntz  33694  tocycval  33717  extvval  34211  sigaval  34791  issiga  34792  issgon  34803  isros  34849  unelros  34852  difelros  34853  inelsros  34859  diffiunisros  34860  rossros  34861  inelcarsg  34991  carsgclctunlem2  34999  probun  35099  ballotlemgval  35204  cvmscbv  36111  cvmsi  36118  cvmsval  36119  poimirlem4  38649  dssmapfvd  45124  compne  45531  dvmptfprod  47062  caragensplit  47617  vonvolmbllem  47777  vonvolmbl  47778  ldepsnlinc  49727