Theorem difeq1 3977

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1508   ∈ wcel 2051  {crab 3087   ∖ cdif 3821

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1744  df-sb 2017  df-clab 2754  df-cleq 2766  df-clel 2841  df-rab 3092  df-dif 3827

This theorem is referenced by:  difeq12  3979  difeq1i  3980  difeq1d  3983  symdifeq1  4103  uneqdifeq  4316  hartogslem1  8800  kmlem9  9377  kmlem11  9379  kmlem12  9380  isfin1a  9511  fin1a2lem13  9631  fundmge2nop0  13660  incexclem  15050  coprmprod  15860  coprmproddvds  15862  ismri  16773  f1otrspeq  18349  pmtrval  18353  pmtrfrn  18360  symgsssg  18369  symgfisg  18370  symggen  18372  psgnunilem1  18395  psgnunilem5  18396  psgnunilem5OLD  18397  psgneldm  18406  ablfac1eulem  18957  sdrgacs  19315  islbs  19583  lbsextlem1  19665  lbsextlem2  19666  lbsextlem3  19667  lbsextlem4  19668  cofipsgn  20455  submafval  20908  m1detdiag  20926  lpval  21467  2ndcdisj  21784  isufil  22231  ptcmplem2  22381  mblsplit  23852  voliunlem3  23872  ig1pval  24485  nbgr2vtx1edg  26851  nbuhgr2vtx1edgb  26853  nbgr0vtx  26857  nb3grprlem2  26882  uvtx01vtx  26898  cplgr1v  26931  dfconngr1  27733  isconngr1  27735  isfrgr  27808  frgr1v  27821  nfrgr2v  27822  frgr3v  27825  1vwmgr  27826  3vfriswmgr  27828  difeq  30072  tocycval  30473  sigaval  31047  issiga  31048  issgon  31060  isros  31105  unelros  31108  difelros  31109  inelsros  31115  diffiunisros  31116  rossros  31117  inelcarsg  31247  carsgclctunlem2  31255  probun  31356  ballotlemgval  31460  cvmscbv  32123  cvmsi  32130  cvmsval  32131  poimirlem4  34370  dssmapfvd  39760  compne  40225  compneOLD  40226  dvmptfprod  41690  caragensplit  42243  vonvolmbllem  42403  vonvolmbl  42404  ldepsnlinc  43960  eenglngeehlnm  44124