Theorem difeq1 4114

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ∈ wcel 2104  {crab 3430   ∖ cdif 3944

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-dif 3950

This theorem is referenced by:  difeq12  4116  difeq1i  4117  difeq1d  4120  symdifeq1  4243  uneqdifeq  4491  hartogslem1  9539  kmlem9  10155  kmlem11  10157  kmlem12  10158  isfin1a  10289  fin1a2lem13  10409  fundmge2nop0  14457  incexclem  15786  coprmprod  16602  coprmproddvds  16604  ismri  17579  f1otrspeq  19356  pmtrval  19360  pmtrfrn  19367  symgsssg  19376  symgfisg  19377  symggen  19379  psgnunilem1  19402  psgnunilem5  19403  psgneldm  19412  ablfac1eulem  19983  sdrgacs  20560  islbs  20831  lbsextlem1  20916  lbsextlem2  20917  lbsextlem3  20918  lbsextlem4  20919  cofipsgn  21365  selvffval  21898  submafval  22301  m1detdiag  22319  lpval  22863  2ndcdisj  23180  isufil  23627  ptcmplem2  23777  mblsplit  25281  voliunlem3  25301  ig1pval  25925  nbgr2vtx1edg  28874  nbuhgr2vtx1edgb  28876  nbgr0vtx  28880  nb3grprlem2  28905  uvtx01vtx  28921  cplgr1v  28954  dfconngr1  29708  isconngr1  29710  isfrgr  29780  frgr1v  29791  nfrgr2v  29792  frgr3v  29795  1vwmgr  29796  3vfriswmgr  29798  difeq  32023  symgcntz  32516  tocycval  32537  sigaval  33407  issiga  33408  issgon  33419  isros  33464  unelros  33467  difelros  33468  inelsros  33474  diffiunisros  33475  rossros  33476  inelcarsg  33608  carsgclctunlem2  33616  probun  33716  ballotlemgval  33820  cvmscbv  34547  cvmsi  34554  cvmsval  34555  poimirlem4  36795  dssmapfvd  43070  compne  43502  dvmptfprod  44959  caragensplit  45514  vonvolmbllem  45674  vonvolmbl  45675  ldepsnlinc  47276  eenglngeehlnm  47512