Theorem difeq1 4046

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ∈ wcel 2108  {crab 3067   ∖ cdif 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-dif 3886

This theorem is referenced by:  difeq12  4048  difeq1i  4049  difeq1d  4052  symdifeq1  4175  uneqdifeq  4420  hartogslem1  9231  kmlem9  9845  kmlem11  9847  kmlem12  9848  isfin1a  9979  fin1a2lem13  10099  fundmge2nop0  14134  incexclem  15476  coprmprod  16294  coprmproddvds  16296  ismri  17257  f1otrspeq  18970  pmtrval  18974  pmtrfrn  18981  symgsssg  18990  symgfisg  18991  symggen  18993  psgnunilem1  19016  psgnunilem5  19017  psgneldm  19026  ablfac1eulem  19590  sdrgacs  19984  islbs  20253  lbsextlem1  20335  lbsextlem2  20336  lbsextlem3  20337  lbsextlem4  20338  cofipsgn  20710  selvffval  21236  submafval  21636  m1detdiag  21654  lpval  22198  2ndcdisj  22515  isufil  22962  ptcmplem2  23112  mblsplit  24601  voliunlem3  24621  ig1pval  25242  nbgr2vtx1edg  27620  nbuhgr2vtx1edgb  27622  nbgr0vtx  27626  nb3grprlem2  27651  uvtx01vtx  27667  cplgr1v  27700  dfconngr1  28453  isconngr1  28455  isfrgr  28525  frgr1v  28536  nfrgr2v  28537  frgr3v  28540  1vwmgr  28541  3vfriswmgr  28543  difeq  30766  symgcntz  31256  tocycval  31277  sigaval  31979  issiga  31980  issgon  31991  isros  32036  unelros  32039  difelros  32040  inelsros  32046  diffiunisros  32047  rossros  32048  inelcarsg  32178  carsgclctunlem2  32186  probun  32286  ballotlemgval  32390  cvmscbv  33120  cvmsi  33127  cvmsval  33128  poimirlem4  35708  dssmapfvd  41514  compne  41948  dvmptfprod  43376  caragensplit  43928  vonvolmbllem  44088  vonvolmbl  44089  ldepsnlinc  45737  eenglngeehlnm  45973