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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2145  {crab 3412   ∖ 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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-dif 3902

This theorem is used by:  difeq12  4069  difeq1i  4070  difeq1d  4073  symdifeq1  4201  uneqdifeq  4448  hartogslem1  9514  kmlem9  10161  kmlem11  10163  kmlem12  10164  isfin1a  10294  fin1a2lem13  10414  fundmge2nop0  14567  incexclem  15925  coprmprod  16751  coprmproddvds  16753  ismri  17719  f1otrspeq  19574  pmtrval  19578  pmtrfrn  19585  symgsssg  19594  symgfisg  19595  symggen  19597  psgnunilem1  19620  psgnunilem5  19621  psgneldm  19630  ablfac1eulem  20201  sdrgacs  20967  islbs  21260  lbsextlem1  21345  lbsextlem2  21346  lbsextlem3  21347  lbsextlem4  21348  cofipsgn  21806  selvffval  22334  submafval  22801  m1detdiag  22819  lpval  23364  2ndcdisj  23682  isufil  24129  ptcmplem2  24279  mblsplit  25760  voliunlem3  25780  ig1pval  26401  nbgr2vtx1edg  29810  nbuhgr2vtx1edgb  29812  nb3grprlem2  29841  uvtx01vtx  29857  cplgr1v  29890  dfconngr1  30668  isconngr1  30670  isfrgr  30740  frgr1v  30751  nfrgr2v  30752  frgr3v  30755  1vwmgr  30756  3vfriswmgr  30758  difeq  32993  symgcntz  33525  tocycval  33548  extvval  34041  sigaval  34621  issiga  34622  issgon  34633  isros  34679  unelros  34682  difelros  34683  inelsros  34689  diffiunisros  34690  rossros  34691  inelcarsg  34822  carsgclctunlem2  34830  probun  34930  ballotlemgval  35035  cvmscbv  35837  cvmsi  35844  cvmsval  35845  poimirlem4  38373  dssmapfvd  44857  compne  45264  dvmptfprod  46773  caragensplit  47328  vonvolmbllem  47488  vonvolmbl  47489  ldepsnlinc  49438  eenglngeehlnm  49669