Theorem difeq1 4064

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ∈ wcel 2111  {crab 3395   ∖ cdif 3894

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-dif 3900

This theorem is referenced by:  difeq12  4066  difeq1i  4067  difeq1d  4070  symdifeq1  4200  uneqdifeq  4438  hartogslem1  9423  kmlem9  10045  kmlem11  10047  kmlem12  10048  isfin1a  10178  fin1a2lem13  10298  fundmge2nop0  14404  incexclem  15738  coprmprod  16567  coprmproddvds  16569  ismri  17532  f1otrspeq  19354  pmtrval  19358  pmtrfrn  19365  symgsssg  19374  symgfisg  19375  symggen  19377  psgnunilem1  19400  psgnunilem5  19401  psgneldm  19410  ablfac1eulem  19981  sdrgacs  20711  islbs  21005  lbsextlem1  21090  lbsextlem2  21091  lbsextlem3  21092  lbsextlem4  21093  cofipsgn  21525  selvffval  22043  submafval  22489  m1detdiag  22507  lpval  23049  2ndcdisj  23366  isufil  23813  ptcmplem2  23963  mblsplit  25455  voliunlem3  25475  ig1pval  26103  nbgr2vtx1edg  29323  nbuhgr2vtx1edgb  29325  nb3grprlem2  29354  uvtx01vtx  29370  cplgr1v  29403  dfconngr1  30160  isconngr1  30162  isfrgr  30232  frgr1v  30243  nfrgr2v  30244  frgr3v  30247  1vwmgr  30248  3vfriswmgr  30250  difeq  32490  symgcntz  33046  tocycval  33069  sigaval  34116  issiga  34117  issgon  34128  isros  34173  unelros  34176  difelros  34177  inelsros  34183  diffiunisros  34184  rossros  34185  inelcarsg  34316  carsgclctunlem2  34324  probun  34424  ballotlemgval  34529  cvmscbv  35294  cvmsi  35301  cvmsval  35302  poimirlem4  37664  dssmapfvd  44050  compne  44473  dvmptfprod  45983  caragensplit  46538  vonvolmbllem  46698  vonvolmbl  46699  ldepsnlinc  48540  eenglngeehlnm  48771