Theorem difeq1 4055

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ∈ wcel 2110  {crab 3070   ∖ cdif 3889

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 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-dif 3895

This theorem is referenced by:  difeq12  4057  difeq1i  4058  difeq1d  4061  symdifeq1  4184  uneqdifeq  4429  hartogslem1  9279  kmlem9  9915  kmlem11  9917  kmlem12  9918  isfin1a  10049  fin1a2lem13  10169  fundmge2nop0  14204  incexclem  15546  coprmprod  16364  coprmproddvds  16366  ismri  17338  f1otrspeq  19053  pmtrval  19057  pmtrfrn  19064  symgsssg  19073  symgfisg  19074  symggen  19076  psgnunilem1  19099  psgnunilem5  19100  psgneldm  19109  ablfac1eulem  19673  sdrgacs  20067  islbs  20336  lbsextlem1  20418  lbsextlem2  20419  lbsextlem3  20420  lbsextlem4  20421  cofipsgn  20796  selvffval  21324  submafval  21726  m1detdiag  21744  lpval  22288  2ndcdisj  22605  isufil  23052  ptcmplem2  23202  mblsplit  24694  voliunlem3  24714  ig1pval  25335  nbgr2vtx1edg  27715  nbuhgr2vtx1edgb  27717  nbgr0vtx  27721  nb3grprlem2  27746  uvtx01vtx  27762  cplgr1v  27795  dfconngr1  28548  isconngr1  28550  isfrgr  28620  frgr1v  28631  nfrgr2v  28632  frgr3v  28635  1vwmgr  28636  3vfriswmgr  28638  difeq  30861  symgcntz  31350  tocycval  31371  sigaval  32075  issiga  32076  issgon  32087  isros  32132  unelros  32135  difelros  32136  inelsros  32142  diffiunisros  32143  rossros  32144  inelcarsg  32274  carsgclctunlem2  32282  probun  32382  ballotlemgval  32486  cvmscbv  33216  cvmsi  33223  cvmsval  33224  poimirlem4  35777  dssmapfvd  41595  compne  42029  dvmptfprod  43457  caragensplit  44009  vonvolmbllem  44169  vonvolmbl  44170  ldepsnlinc  45818  eenglngeehlnm  46054