Theorem difeq1 4050

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ∈ wcel 2119  {crab 3391   ∖ cdif 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-dif 3886

This theorem is referenced by:  difeq12  4052  difeq1i  4053  difeq1d  4056  symdifeq1  4183  uneqdifeq  4420  hartogslem1  9447  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  20773  islbs  21066  lbsextlem1  21151  lbsextlem2  21152  lbsextlem3  21153  lbsextlem4  21154  cofipsgn  21568  selvffval  22094  submafval  22562  m1detdiag  22580  lpval  23122  2ndcdisj  23439  isufil  23886  ptcmplem2  24036  mblsplit  25517  voliunlem3  25537  ig1pval  26159  nbgr2vtx1edg  29437  nbuhgr2vtx1edgb  29439  nb3grprlem2  29468  uvtx01vtx  29484  cplgr1v  29517  dfconngr1  30276  isconngr1  30278  isfrgr  30348  frgr1v  30359  nfrgr2v  30360  frgr3v  30363  1vwmgr  30364  3vfriswmgr  30366  difeq  32606  symgcntz  33166  tocycval  33189  extvval  33715  sigaval  34295  issiga  34296  issgon  34307  isros  34352  unelros  34355  difelros  34356  inelsros  34362  diffiunisros  34363  rossros  34364  inelcarsg  34495  carsgclctunlem2  34503  probun  34603  ballotlemgval  34708  cvmscbv  35486  cvmsi  35493  cvmsval  35494  poimirlem4  37991  dssmapfvd  44461  compne  44884  dvmptfprod  46388  caragensplit  46943  vonvolmbllem  47103  vonvolmbl  47104  ldepsnlinc  48999  eenglngeehlnm  49230