Theorem difeq1 4119

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-dif 3954

This theorem is referenced by:  difeq12  4121  difeq1i  4122  difeq1d  4125  symdifeq1  4255  uneqdifeq  4493  hartogslem1  9582  kmlem9  10199  kmlem11  10201  kmlem12  10202  isfin1a  10332  fin1a2lem13  10452  fundmge2nop0  14541  incexclem  15872  coprmprod  16698  coprmproddvds  16700  ismri  17674  f1otrspeq  19465  pmtrval  19469  pmtrfrn  19476  symgsssg  19485  symgfisg  19486  symggen  19488  psgnunilem1  19511  psgnunilem5  19512  psgneldm  19521  ablfac1eulem  20092  sdrgacs  20802  islbs  21075  lbsextlem1  21160  lbsextlem2  21161  lbsextlem3  21162  lbsextlem4  21163  cofipsgn  21611  selvffval  22137  submafval  22585  m1detdiag  22603  lpval  23147  2ndcdisj  23464  isufil  23911  ptcmplem2  24061  mblsplit  25567  voliunlem3  25587  ig1pval  26215  nbgr2vtx1edg  29367  nbuhgr2vtx1edgb  29369  nb3grprlem2  29398  uvtx01vtx  29414  cplgr1v  29447  dfconngr1  30207  isconngr1  30209  isfrgr  30279  frgr1v  30290  nfrgr2v  30291  frgr3v  30294  1vwmgr  30295  3vfriswmgr  30297  difeq  32537  symgcntz  33105  tocycval  33128  sigaval  34112  issiga  34113  issgon  34124  isros  34169  unelros  34172  difelros  34173  inelsros  34179  diffiunisros  34180  rossros  34181  inelcarsg  34313  carsgclctunlem2  34321  probun  34421  ballotlemgval  34526  cvmscbv  35263  cvmsi  35270  cvmsval  35271  poimirlem4  37631  dssmapfvd  44030  compne  44460  dvmptfprod  45960  caragensplit  46515  vonvolmbllem  46675  vonvolmbl  46676  ldepsnlinc  48425  eenglngeehlnm  48660