Theorem difeq1 4059

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ∈ wcel 2147  {crab 3416   ∖ cdif 4048

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-dif 4050

This theorem is used by:  difeq12  4061  difeq1i  4062  difeq1d  4065  symdifeq1  4203  uneqdifeq  4451  hartogslem1  9573  kmlem9  10276  kmlem11  10278  kmlem12  10279  isfin1a  10409  fin1a2lem13  10529  fundmge2nop0  14688  incexclem  16049  coprmprod  16880  coprmproddvds  16882  ismri  17855  f1otrspeq  19712  pmtrval  19716  pmtrfrn  19723  symgsssg  19732  symgfisg  19733  symggen  19735  psgnunilem1  19758  psgnunilem5  19759  psgneldm  19768  ablfac1eulem  20339  sdrgacs  21109  islbs  21402  lbsextlem1  21487  lbsextlem2  21488  lbsextlem3  21489  lbsextlem4  21490  cofipsgn  21954  selvffval  22482  submafval  22949  m1detdiag  22967  lpval  23512  2ndcdisj  23830  isufil  24277  ptcmplem2  24427  mblsplit  25908  voliunlem3  25928  ig1pval  26549  nbgr2vtx1edg  29988  nbuhgr2vtx1edgb  29990  nb3grprlem2  30019  uvtx01vtx  30035  cplgr1v  30068  dfconngr1  30846  isconngr1  30848  isfrgr  30918  frgr1v  30929  nfrgr2v  30930  frgr3v  30933  1vwmgr  30934  3vfriswmgr  30936  difeq  33213  symgcntz  33745  tocycval  33768  extvval  34274  sigaval  34854  issiga  34855  issgon  34866  isros  34912  unelros  34915  difelros  34916  inelsros  34922  diffiunisros  34923  rossros  34924  inelcarsg  35054  carsgclctunlem2  35062  probun  35162  ballotlemgval  35267  gdlop3fv  36006  cvmscbv  36231  cvmsi  36238  cvmsval  36239  poimirlem4  38810  dssmapfvd  45278  compne  45684  dvmptfprod  47228  caragensplit  47783  vonvolmbllem  47943  vonvolmbl  47944  ldepsnlinc  49951