Theorem difeq1 4082

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1567   ∈ wcel 2149  {crab 3423   ∖ cdif 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-dif 3916

This theorem is referenced by:  difeq12  4084  difeq1i  4085  difeq1d  4088  symdifeq1  4216  uneqdifeq  4455  hartogslem1  9500  kmlem9  10138  kmlem11  10140  kmlem12  10141  isfin1a  10272  fin1a2lem13  10392  fundmge2nop0  14535  incexclem  15886  coprmprod  16715  coprmproddvds  16717  ismri  17683  f1otrspeq  19513  pmtrval  19517  pmtrfrn  19524  symgsssg  19533  symgfisg  19534  symggen  19536  psgnunilem1  19559  psgnunilem5  19560  psgneldm  19569  ablfac1eulem  20140  sdrgacs  20878  islbs  21171  lbsextlem1  21256  lbsextlem2  21257  lbsextlem3  21258  lbsextlem4  21259  cofipsgn  21708  selvffval  22234  submafval  22701  m1detdiag  22719  lpval  23261  2ndcdisj  23578  isufil  24025  ptcmplem2  24175  mblsplit  25656  voliunlem3  25676  ig1pval  26298  nbgr2vtx1edg  29637  nbuhgr2vtx1edgb  29639  nb3grprlem2  29668  uvtx01vtx  29684  cplgr1v  29717  dfconngr1  30476  isconngr1  30478  isfrgr  30548  frgr1v  30559  nfrgr2v  30560  frgr3v  30563  1vwmgr  30564  3vfriswmgr  30566  difeq  32801  symgcntz  33342  tocycval  33365  extvval  33862  sigaval  34442  issiga  34443  issgon  34454  isros  34499  unelros  34502  difelros  34503  inelsros  34509  diffiunisros  34510  rossros  34511  inelcarsg  34642  carsgclctunlem2  34650  probun  34750  ballotlemgval  34855  cvmscbv  35645  cvmsi  35652  cvmsval  35653  poimirlem4  38158  dssmapfvd  44630  compne  45037  dvmptfprod  46546  caragensplit  47101  vonvolmbllem  47261  vonvolmbl  47262  ldepsnlinc  49168  eenglngeehlnm  49399