Theorem difeq1 4074

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2146  {crab 3418   ∖ cdif 3903

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-dif 3909

This theorem is used by:  difeq12  4076  difeq1i  4077  difeq1d  4080  symdifeq1  4208  uneqdifeq  4455  hartogslem1  9511  kmlem9  10158  kmlem11  10160  kmlem12  10161  isfin1a  10291  fin1a2lem13  10411  fundmge2nop0  14557  incexclem  15913  coprmprod  16741  coprmproddvds  16743  ismri  17709  f1otrspeq  19561  pmtrval  19565  pmtrfrn  19572  symgsssg  19581  symgfisg  19582  symggen  19584  psgnunilem1  19607  psgnunilem5  19608  psgneldm  19617  ablfac1eulem  20188  sdrgacs  20954  islbs  21247  lbsextlem1  21332  lbsextlem2  21333  lbsextlem3  21334  lbsextlem4  21335  cofipsgn  21793  selvffval  22319  submafval  22786  m1detdiag  22804  lpval  23346  2ndcdisj  23664  isufil  24111  ptcmplem2  24261  mblsplit  25742  voliunlem3  25762  ig1pval  26384  nbgr2vtx1edg  29758  nbuhgr2vtx1edgb  29760  nb3grprlem2  29789  uvtx01vtx  29805  cplgr1v  29838  dfconngr1  30610  isconngr1  30612  isfrgr  30682  frgr1v  30693  nfrgr2v  30694  frgr3v  30697  1vwmgr  30698  3vfriswmgr  30700  difeq  32935  symgcntz  33469  tocycval  33492  extvval  33985  sigaval  34565  issiga  34566  issgon  34577  isros  34623  unelros  34626  difelros  34627  inelsros  34633  diffiunisros  34634  rossros  34635  inelcarsg  34766  carsgclctunlem2  34774  probun  34874  ballotlemgval  34979  cvmscbv  35787  cvmsi  35794  cvmsval  35795  poimirlem4  38332  dssmapfvd  44801  compne  45208  dvmptfprod  46717  caragensplit  47272  vonvolmbllem  47432  vonvolmbl  47433  ldepsnlinc  49345  eenglngeehlnm  49576