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

Theorem difeq1 3754
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 3223 . 2 (𝐴 = 𝐵 → {𝑥𝐴 ∣ ¬ 𝑥𝐶} = {𝑥𝐵 ∣ ¬ 𝑥𝐶})
2 dfdif2 3616 . 2 (𝐴𝐶) = {𝑥𝐴 ∣ ¬ 𝑥𝐶}
3 dfdif2 3616 . 2 (𝐵𝐶) = {𝑥𝐵 ∣ ¬ 𝑥𝐶}
41, 2, 33eqtr4g 2710 1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1523  wcel 2030  {crab 2945  cdif 3604
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-dif 3610
This theorem is referenced by:  difeq12  3756  difeq1i  3757  difeq1d  3760  symdifeq1  3879  uneqdifeq  4090  uneqdifeqOLD  4091  hartogslem1  8488  kmlem9  9018  kmlem11  9020  kmlem12  9021  isfin1a  9152  fin1a2lem13  9272  fundmge2nop0  13312  incexclem  14612  coprmprod  15422  coprmproddvds  15424  ismri  16338  f1otrspeq  17913  pmtrval  17917  pmtrfrn  17924  symgsssg  17933  symgfisg  17934  symggen  17936  psgnunilem1  17959  psgnunilem5  17960  psgneldm  17969  ablfac1eulem  18517  islbs  19124  lbsextlem1  19206  lbsextlem2  19207  lbsextlem3  19208  lbsextlem4  19209  zrhcofipsgn  19987  submafval  20433  m1detdiag  20451  lpval  20991  2ndcdisj  21307  isufil  21754  ptcmplem2  21904  mblsplit  23346  voliunlem3  23366  ig1pval  23977  nbgr2vtx1edg  26291  nbuhgr2vtx1edgb  26293  nbgr0vtx  26297  nb3grprlem2  26327  uvtx01vtx  26346  uvtxa01vtx0OLD  26348  cplgr1v  26382  dfconngr1  27166  isconngr1  27168  isfrgr  27238  frgr1v  27251  nfrgr2v  27252  frgr3v  27255  1vwmgr  27256  3vfriswmgr  27258  difeq  29481  sigaval  30301  issiga  30302  issgon  30314  isros  30359  unelros  30362  difelros  30363  inelsros  30369  diffiunisros  30370  rossros  30371  inelcarsg  30501  carsgclctunlem2  30509  probun  30609  ballotlemgval  30713  cvmscbv  31366  cvmsi  31373  cvmsval  31374  poimirlem4  33543  sdrgacs  38088  dssmapfvd  38628  compne  38960  compneOLD  38961  dvmptfprod  40478  caragensplit  41035  vonvolmbllem  41195  vonvolmbl  41196  ldepsnlinc  42622
  Copyright terms: Public domain W3C validator