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

Theorem ineq1d 3956
Description: Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.)
Hypothesis
Ref Expression
ineq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
ineq1d (𝜑 → (𝐴𝐶) = (𝐵𝐶))

Proof of Theorem ineq1d
StepHypRef Expression
1 ineq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 ineq1 3950 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  cin 3714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-in 3722
This theorem is referenced by:  diftpsn3OLD  4478  iinrab2  4735  disji2  4788  disjprg  4800  disjxun  4802  riinint  5537  fnresdisj  6162  fnimadisj  6173  fninfp  6604  ecinxp  7989  fiint  8402  fival  8483  marypha1lem  8504  kmlem12  9175  fin23lem12  9345  fin23lem30  9356  fin23lem33  9359  ttukeylem1  9523  fpwwe2cbv  9644  fpwwe2lem2  9646  fpwwe2  9657  fzval2  12522  fvinim0ffz  12781  limsupval  14404  limsupgval  14406  ello1  14445  elo1  14456  fsum1p  14681  incexclem  14767  fprod1p  14897  smuval2  15406  smueqlem  15414  smumul  15417  setsdm  16094  isacs2  16515  acsfiel  16516  isacs1i  16519  catcval  16947  resscatc  16956  acsficl  17372  lsmdisj3  18296  lsmdisj3a  18302  dprdres  18627  dprdz  18629  dpjdisj  18652  lspdisj2  19329  indistopon  21007  restopnb  21181  ordtrest2  21210  isnrm  21341  cmpcov  21394  cmpsublem  21404  cmpsub  21405  tgcmp  21406  uncmp  21408  hauscmplem  21411  nconnsubb  21428  isnlly  21474  dissnlocfin  21534  kgeni  21542  kgencn3  21563  ptcld  21618  ptcnplem  21626  alexsublem  22049  alexsubb  22051  alexsubALTlem2  22053  alexsubALTlem4  22055  alexsubALT  22056  tmdgsum2  22101  tsmsval2  22134  ustexsym  22220  metrest  22530  qtopbaslem  22763  cnheibor  22955  bndth  22958  lebnumii  22966  iscph  23170  csscld  23248  clsocv  23249  ovolicc2  23490  voliunlem3  23520  ioombl  23533  uniioombllem2  23551  uniioombllem4  23554  uniioombllem6  23556  mbflimsup  23632  taylfval  24312  chtval  25035  ppival  25052  ppival2  25053  ppival2g  25054  chtfl  25074  ppiprm  25076  chtprm  25078  chtnprm  25079  chtdif  25083  ppidif  25088  prmorcht  25103  chdmj2  28698  cmcmlem  28759  pjoml2  28779  fh2  28787  mdbr  29462  mdi  29463  mdbr3  29465  mdbr4  29466  dmdmd  29468  dmdbr3  29473  dmdbr4  29474  dmdi4  29475  dmdbr5  29476  mddmd2  29477  mdsl1i  29489  cvmdi  29492  mdslmd1lem1  29493  mdslmd1lem2  29494  mdslmd1lem3  29495  mdslmd1lem4  29496  mdslmd1i  29497  mdslmd3i  29500  csmdsymi  29502  mdexchi  29503  atomli  29550  atabsi  29569  sumdmdlem2  29587  dmdbr5ati  29590  difuncomp  29676  disji2f  29697  disjif2  29701  disjxpin  29708  disjunsn  29714  fnresin  29739  locfinreflem  30216  iscref  30220  ordtrest2NEW  30278  ordtconnlem1  30279  carsgclctunlem1  30688  totprobd  30797  probmeasb  30801  ballotlemfval  30860  ballotlemfp1  30862  ballotlemgun  30895  chtvalz  31016  bnj1385  31210  bnj1326  31401  iccllysconn  31539  mvrsval  31709  mrsubvrs  31726  mpstval  31739  msubvrs  31764  nosupbnd2lem1  32167  neibastop2lem  32661  neibastop2  32662  neibastop3  32663  limsucncmpi  32750  bj-ismoore  33365  ptrest  33721  mblfinlem2  33760  sstotbnd2  33886  cntotbnd  33908  heibor  33933  xrneq1  34462  l1cvat  34845  pmodlem2  35636  pmod2iN  35638  hlmod1i  35645  osumcllem3N  35747  osumcllem9N  35753  pexmidlem6N  35764  pl42lem1N  35768  istrnN  35947  djavalN  36926  dihmeetlem9N  37106  dihmeetlem11N  37108  dihmeetlem12N  37109  dihoml4  37168  djhval  37189  dochexmidlem6  37256  lclkrlem2b  37299  lcfrlem20  37353  lcfrlem23  37356  elrfi  37759  isnacs  37769  mrefg2  37772  mapfzcons2  37784  coeq0i  37818  eldioph2lem2  37826  aomclem8  38133  kelac1  38135  islmodfg  38141  lnr2i  38188  fgraphopab  38290  ntrkbimka  38838  ntrk0kbimka  38839  isotone2  38849  ntrclskb  38869  ntrclsk3  38870  ntrclsk13  38871  neicvgbex  38912  disjrnmpt2  39874  disjinfi  39879  uzinico2  40292  uzinico3  40293  fsumiunss  40310  lptre2pt  40375  limsupresre  40431  limsuplesup  40434  limsupresico  40435  limsupvaluz  40443  limsuplt2  40488  liminfval  40494  limsupge  40496  liminfgval  40497  liminfval2  40503  liminfresico  40506  liminflelimsuplem  40510  liminflelimsup  40511  stoweidlem50  40770  stoweidlem57  40777  subsaliuncllem  41078  sge0val  41086  sge0iunmptlemre  41135  nnfoctbdjlem  41175  iundjiun  41180  vonvolmbllem  41380  smfpimcclem  41519  smfsuplem1  41523  elbigo  42855  aacllem  43060
  Copyright terms: Public domain W3C validator