Theorem difeq1 4060

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ∈ wcel 2114  {crab 3390   ∖ cdif 3887

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-dif 3893

This theorem is referenced by:  difeq12  4062  difeq1i  4063  difeq1d  4066  symdifeq1  4196  uneqdifeq  4433  hartogslem1  9450  kmlem9  10072  kmlem11  10074  kmlem12  10075  isfin1a  10205  fin1a2lem13  10325  fundmge2nop0  14455  incexclem  15792  coprmprod  16621  coprmproddvds  16623  ismri  17588  f1otrspeq  19413  pmtrval  19417  pmtrfrn  19424  symgsssg  19433  symgfisg  19434  symggen  19436  psgnunilem1  19459  psgnunilem5  19460  psgneldm  19469  ablfac1eulem  20040  sdrgacs  20769  islbs  21063  lbsextlem1  21148  lbsextlem2  21149  lbsextlem3  21150  lbsextlem4  21151  cofipsgn  21583  selvffval  22109  submafval  22554  m1detdiag  22572  lpval  23114  2ndcdisj  23431  isufil  23878  ptcmplem2  24028  mblsplit  25509  voliunlem3  25529  ig1pval  26151  nbgr2vtx1edg  29433  nbuhgr2vtx1edgb  29435  nb3grprlem2  29464  uvtx01vtx  29480  cplgr1v  29513  dfconngr1  30273  isconngr1  30275  isfrgr  30345  frgr1v  30356  nfrgr2v  30357  frgr3v  30360  1vwmgr  30361  3vfriswmgr  30363  difeq  32603  symgcntz  33161  tocycval  33184  extvval  33690  sigaval  34271  issiga  34272  issgon  34283  isros  34328  unelros  34331  difelros  34332  inelsros  34338  diffiunisros  34339  rossros  34340  inelcarsg  34471  carsgclctunlem2  34479  probun  34579  ballotlemgval  34684  cvmscbv  35456  cvmsi  35463  cvmsval  35464  poimirlem4  37959  dssmapfvd  44462  compne  44885  dvmptfprod  46391  caragensplit  46946  vonvolmbllem  47106  vonvolmbl  47107  ldepsnlinc  48996  eenglngeehlnm  49227