Theorem difeq1 4142

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ∈ wcel 2108  {crab 3443   ∖ cdif 3973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-dif 3979

This theorem is referenced by:  difeq12  4144  difeq1i  4145  difeq1d  4148  symdifeq1  4274  uneqdifeq  4516  hartogslem1  9611  kmlem9  10228  kmlem11  10230  kmlem12  10231  isfin1a  10361  fin1a2lem13  10481  fundmge2nop0  14551  incexclem  15884  coprmprod  16708  coprmproddvds  16710  ismri  17689  f1otrspeq  19489  pmtrval  19493  pmtrfrn  19500  symgsssg  19509  symgfisg  19510  symggen  19512  psgnunilem1  19535  psgnunilem5  19536  psgneldm  19545  ablfac1eulem  20116  sdrgacs  20824  islbs  21098  lbsextlem1  21183  lbsextlem2  21184  lbsextlem3  21185  lbsextlem4  21186  cofipsgn  21634  selvffval  22160  submafval  22606  m1detdiag  22624  lpval  23168  2ndcdisj  23485  isufil  23932  ptcmplem2  24082  mblsplit  25586  voliunlem3  25606  ig1pval  26235  nbgr2vtx1edg  29385  nbuhgr2vtx1edgb  29387  nb3grprlem2  29416  uvtx01vtx  29432  cplgr1v  29465  dfconngr1  30220  isconngr1  30222  isfrgr  30292  frgr1v  30303  nfrgr2v  30304  frgr3v  30307  1vwmgr  30308  3vfriswmgr  30310  difeq  32548  symgcntz  33078  tocycval  33101  sigaval  34075  issiga  34076  issgon  34087  isros  34132  unelros  34135  difelros  34136  inelsros  34142  diffiunisros  34143  rossros  34144  inelcarsg  34276  carsgclctunlem2  34284  probun  34384  ballotlemgval  34488  cvmscbv  35226  cvmsi  35233  cvmsval  35234  poimirlem4  37584  dssmapfvd  43979  compne  44410  dvmptfprod  45866  caragensplit  46421  vonvolmbllem  46581  vonvolmbl  46582  ldepsnlinc  48237  eenglngeehlnm  48473