Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  difeq1 Structured version   Visualization version   GIF version

Theorem difeq1 3713
 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.
StepHypRef Expression
1 rabeq 3187 . 2 (𝐴 = 𝐵 → {𝑥𝐴 ∣ ¬ 𝑥𝐶} = {𝑥𝐵 ∣ ¬ 𝑥𝐶})
2 dfdif2 3576 . 2 (𝐴𝐶) = {𝑥𝐴 ∣ ¬ 𝑥𝐶}
3 dfdif2 3576 . 2 (𝐵𝐶) = {𝑥𝐵 ∣ ¬ 𝑥𝐶}
41, 2, 33eqtr4g 2679 1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1481   ∈ wcel 1988  {crab 2913   ∖ cdif 3564 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rab 2918  df-dif 3570 This theorem is referenced by:  difeq12  3715  difeq1i  3716  difeq1d  3719  symdifeq1  3838  uneqdifeq  4048  uneqdifeqOLD  4049  hartogslem1  8432  kmlem9  8965  kmlem11  8967  kmlem12  8968  isfin1a  9099  fin1a2lem13  9219  fundmge2nop0  13257  incexclem  14549  coprmprod  15356  coprmproddvds  15358  ismri  16272  f1otrspeq  17848  pmtrval  17852  pmtrfrn  17859  symgsssg  17868  symgfisg  17869  symggen  17871  psgnunilem1  17894  psgnunilem5  17895  psgneldm  17904  ablfac1eulem  18452  islbs  19057  lbsextlem1  19139  lbsextlem2  19140  lbsextlem3  19141  lbsextlem4  19142  zrhcofipsgn  19920  submafval  20366  m1detdiag  20384  lpval  20924  2ndcdisj  21240  isufil  21688  ptcmplem2  21838  mblsplit  23281  voliunlem3  23301  ig1pval  23913  nbgr2vtx1edg  26227  nbuhgr2vtx1edgb  26229  nbgr0vtx  26233  nb3grprlem2  26264  uvtxa01vtx0  26278  cplgr1v  26307  dfconngr1  27028  isconngr1  27030  isfrgr  27102  frgr1v  27115  nfrgr2v  27116  frgr3v  27119  1vwmgr  27120  3vfriswmgr  27122  difeq  29327  sigaval  30147  issiga  30148  issgon  30160  isros  30205  unelros  30208  difelros  30209  inelsros  30215  diffiunisros  30216  rossros  30217  inelcarsg  30347  carsgclctunlem2  30355  probun  30455  ballotlemgval  30559  cvmscbv  31214  cvmsi  31221  cvmsval  31222  poimirlem4  33384  sdrgacs  37590  dssmapfvd  38131  compne  38463  compneOLD  38464  dvmptfprod  39923  caragensplit  40477  vonvolmbllem  40637  vonvolmbl  40638  ldepsnlinc  42062
 Copyright terms: Public domain W3C validator