Theorem difeq1 4112

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1534   ∈ wcel 2099  {crab 3428   ∖ cdif 3942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3429  df-dif 3948

This theorem is referenced by:  difeq12  4114  difeq1i  4115  difeq1d  4118  symdifeq1  4241  uneqdifeq  4489  hartogslem1  9560  kmlem9  10176  kmlem11  10178  kmlem12  10179  isfin1a  10310  fin1a2lem13  10430  fundmge2nop0  14480  incexclem  15809  coprmprod  16626  coprmproddvds  16628  ismri  17605  f1otrspeq  19396  pmtrval  19400  pmtrfrn  19407  symgsssg  19416  symgfisg  19417  symggen  19419  psgnunilem1  19442  psgnunilem5  19443  psgneldm  19452  ablfac1eulem  20023  sdrgacs  20683  islbs  20955  lbsextlem1  21040  lbsextlem2  21041  lbsextlem3  21042  lbsextlem4  21043  cofipsgn  21519  selvffval  22053  submafval  22475  m1detdiag  22493  lpval  23037  2ndcdisj  23354  isufil  23801  ptcmplem2  23951  mblsplit  25455  voliunlem3  25475  ig1pval  26104  nbgr2vtx1edg  29157  nbuhgr2vtx1edgb  29159  nbgr0vtx  29163  nb3grprlem2  29188  uvtx01vtx  29204  cplgr1v  29237  dfconngr1  29992  isconngr1  29994  isfrgr  30064  frgr1v  30075  nfrgr2v  30076  frgr3v  30079  1vwmgr  30080  3vfriswmgr  30082  difeq  32309  symgcntz  32803  tocycval  32824  sigaval  33725  issiga  33726  issgon  33737  isros  33782  unelros  33785  difelros  33786  inelsros  33792  diffiunisros  33793  rossros  33794  inelcarsg  33926  carsgclctunlem2  33934  probun  34034  ballotlemgval  34138  cvmscbv  34863  cvmsi  34870  cvmsval  34871  poimirlem4  37092  dssmapfvd  43438  compne  43869  dvmptfprod  45324  caragensplit  45879  vonvolmbllem  46039  vonvolmbl  46040  ldepsnlinc  47567  eenglngeehlnm  47803