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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2143  {crab 3416   ∖ cdif 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-dif 3908

This theorem is referenced by:  difeq12  4076  difeq1i  4077  difeq1d  4080  symdifeq1  4208  uneqdifeq  4453  hartogslem1  9500  kmlem9  10138  kmlem11  10140  kmlem12  10141  isfin1a  10271  fin1a2lem13  10391  fundmge2nop0  14535  incexclem  15886  coprmprod  16714  coprmproddvds  16716  ismri  17682  f1otrspeq  19512  pmtrval  19516  pmtrfrn  19523  symgsssg  19532  symgfisg  19533  symggen  19535  psgnunilem1  19558  psgnunilem5  19559  psgneldm  19568  ablfac1eulem  20139  sdrgacs  20904  islbs  21197  lbsextlem1  21282  lbsextlem2  21283  lbsextlem3  21284  lbsextlem4  21285  cofipsgn  21743  selvffval  22269  submafval  22736  m1detdiag  22754  lpval  23296  2ndcdisj  23613  isufil  24060  ptcmplem2  24210  mblsplit  25691  voliunlem3  25711  ig1pval  26333  nbgr2vtx1edg  29700  nbuhgr2vtx1edgb  29702  nb3grprlem2  29731  uvtx01vtx  29747  cplgr1v  29780  dfconngr1  30539  isconngr1  30541  isfrgr  30611  frgr1v  30622  nfrgr2v  30623  frgr3v  30626  1vwmgr  30627  3vfriswmgr  30629  difeq  32864  symgcntz  33405  tocycval  33428  extvval  33921  sigaval  34501  issiga  34502  issgon  34513  isros  34558  unelros  34561  difelros  34562  inelsros  34568  diffiunisros  34569  rossros  34570  inelcarsg  34701  carsgclctunlem2  34709  probun  34809  ballotlemgval  34914  cvmscbv  35750  cvmsi  35757  cvmsval  35758  poimirlem4  38275  dssmapfvd  44743  compne  45150  dvmptfprod  46659  caragensplit  47214  vonvolmbllem  47374  vonvolmbl  47375  ldepsnlinc  49288  eenglngeehlnm  49519