Theorem difeq1 4080

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ∈ wcel 2106  {crab 3405   ∖ cdif 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-dif 3916

This theorem is referenced by:  difeq12  4082  difeq1i  4083  difeq1d  4086  symdifeq1  4209  uneqdifeq  4455  hartogslem1  9487  kmlem9  10103  kmlem11  10105  kmlem12  10106  isfin1a  10237  fin1a2lem13  10357  fundmge2nop0  14403  incexclem  15732  coprmprod  16548  coprmproddvds  16550  ismri  17525  f1otrspeq  19243  pmtrval  19247  pmtrfrn  19254  symgsssg  19263  symgfisg  19264  symggen  19266  psgnunilem1  19289  psgnunilem5  19290  psgneldm  19299  ablfac1eulem  19865  sdrgacs  20324  islbs  20594  lbsextlem1  20678  lbsextlem2  20679  lbsextlem3  20680  lbsextlem4  20681  cofipsgn  21034  selvffval  21563  submafval  21965  m1detdiag  21983  lpval  22527  2ndcdisj  22844  isufil  23291  ptcmplem2  23441  mblsplit  24933  voliunlem3  24953  ig1pval  25574  nbgr2vtx1edg  28361  nbuhgr2vtx1edgb  28363  nbgr0vtx  28367  nb3grprlem2  28392  uvtx01vtx  28408  cplgr1v  28441  dfconngr1  29195  isconngr1  29197  isfrgr  29267  frgr1v  29278  nfrgr2v  29279  frgr3v  29282  1vwmgr  29283  3vfriswmgr  29285  difeq  31509  symgcntz  32006  tocycval  32027  sigaval  32799  issiga  32800  issgon  32811  isros  32856  unelros  32859  difelros  32860  inelsros  32866  diffiunisros  32867  rossros  32868  inelcarsg  33000  carsgclctunlem2  33008  probun  33108  ballotlemgval  33212  cvmscbv  33939  cvmsi  33946  cvmsval  33947  poimirlem4  36155  dssmapfvd  42411  compne  42843  dvmptfprod  44306  caragensplit  44861  vonvolmbllem  45021  vonvolmbl  45022  ldepsnlinc  46709  eenglngeehlnm  46945