Theorem difeq1 4068

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ∈ wcel 2113  {crab 3396   ∖ cdif 3895

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 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-dif 3901

This theorem is referenced by:  difeq12  4070  difeq1i  4071  difeq1d  4074  symdifeq1  4204  uneqdifeq  4442  hartogslem1  9439  kmlem9  10061  kmlem11  10063  kmlem12  10064  isfin1a  10194  fin1a2lem13  10314  fundmge2nop0  14416  incexclem  15750  coprmprod  16579  coprmproddvds  16581  ismri  17545  f1otrspeq  19367  pmtrval  19371  pmtrfrn  19378  symgsssg  19387  symgfisg  19388  symggen  19390  psgnunilem1  19413  psgnunilem5  19414  psgneldm  19423  ablfac1eulem  19994  sdrgacs  20725  islbs  21019  lbsextlem1  21104  lbsextlem2  21105  lbsextlem3  21106  lbsextlem4  21107  cofipsgn  21539  selvffval  22067  submafval  22514  m1detdiag  22532  lpval  23074  2ndcdisj  23391  isufil  23838  ptcmplem2  23988  mblsplit  25480  voliunlem3  25500  ig1pval  26128  nbgr2vtx1edg  29349  nbuhgr2vtx1edgb  29351  nb3grprlem2  29380  uvtx01vtx  29396  cplgr1v  29429  dfconngr1  30189  isconngr1  30191  isfrgr  30261  frgr1v  30272  nfrgr2v  30273  frgr3v  30276  1vwmgr  30277  3vfriswmgr  30279  difeq  32519  symgcntz  33095  tocycval  33118  extvval  33624  sigaval  34196  issiga  34197  issgon  34208  isros  34253  unelros  34256  difelros  34257  inelsros  34263  diffiunisros  34264  rossros  34265  inelcarsg  34396  carsgclctunlem2  34404  probun  34504  ballotlemgval  34609  cvmscbv  35374  cvmsi  35381  cvmsval  35382  poimirlem4  37737  dssmapfvd  44174  compne  44597  dvmptfprod  46105  caragensplit  46660  vonvolmbllem  46820  vonvolmbl  46821  ldepsnlinc  48670  eenglngeehlnm  48901