Theorem difeq1 4094

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ∈ wcel 2108  {crab 3415   ∖ cdif 3923

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-dif 3929

This theorem is referenced by:  difeq12  4096  difeq1i  4097  difeq1d  4100  symdifeq1  4230  uneqdifeq  4468  hartogslem1  9554  kmlem9  10171  kmlem11  10173  kmlem12  10174  isfin1a  10304  fin1a2lem13  10424  fundmge2nop0  14518  incexclem  15850  coprmprod  16678  coprmproddvds  16680  ismri  17641  f1otrspeq  19426  pmtrval  19430  pmtrfrn  19437  symgsssg  19446  symgfisg  19447  symggen  19449  psgnunilem1  19472  psgnunilem5  19473  psgneldm  19482  ablfac1eulem  20053  sdrgacs  20759  islbs  21032  lbsextlem1  21117  lbsextlem2  21118  lbsextlem3  21119  lbsextlem4  21120  cofipsgn  21551  selvffval  22069  submafval  22515  m1detdiag  22533  lpval  23075  2ndcdisj  23392  isufil  23839  ptcmplem2  23989  mblsplit  25483  voliunlem3  25503  ig1pval  26131  nbgr2vtx1edg  29275  nbuhgr2vtx1edgb  29277  nb3grprlem2  29306  uvtx01vtx  29322  cplgr1v  29355  dfconngr1  30115  isconngr1  30117  isfrgr  30187  frgr1v  30198  nfrgr2v  30199  frgr3v  30202  1vwmgr  30203  3vfriswmgr  30205  difeq  32445  symgcntz  33042  tocycval  33065  sigaval  34088  issiga  34089  issgon  34100  isros  34145  unelros  34148  difelros  34149  inelsros  34155  diffiunisros  34156  rossros  34157  inelcarsg  34289  carsgclctunlem2  34297  probun  34397  ballotlemgval  34502  cvmscbv  35226  cvmsi  35233  cvmsval  35234  poimirlem4  37594  dssmapfvd  43988  compne  44413  dvmptfprod  45922  caragensplit  46477  vonvolmbllem  46637  vonvolmbl  46638  ldepsnlinc  48432  eenglngeehlnm  48667