Theorem ineq2d 3699

Description: Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.)

Hypothesis

Ref	Expression
ineq1d.1

Assertion

Ref	Expression
ineq2d

Proof of Theorem ineq2d

Step	Hyp	Ref	Expression
1		ineq1d.1	. 2
2		ineq2 3693	. 2
3	1, 2	syl 16	1

Syntax hints:  ->wi 4  =wceq 1395  i^icin 3474

This theorem is referenced by:  disjpr2  4092  rint0  4327  riin0  4404  disji2  4439  disjprg  4448  disjxun  4450  onfr  4922  xpriindi  5144  riinint  5264  reseq2  5273  csbresgOLD  5282  resindm  5323  isofrlem  6236  isoselem  6237  oev2  7192  domss2  7696  funsnfsupp  7873  kmlem11  8561  fpwwe2cbv  9029  fpwwe2lem3  9032  fpwwe2lem8  9036  fpwwe2lem12  9040  fpwwe2lem13  9041  fpwwe2  9042  fz1isolem  12510  limsupgle  13300  fsumm1  13566  incexclem  13648  bitsinv1  14092  bitsinvp1  14099  sadcadd  14108  sadadd2  14110  smumullem  14142  ressbas  14687  ressress  14694  restval  14824  ismred2  15000  resscatc  15432  cnvps  15842  cntziinsn  16372  lsmdisj3r  16704  lsmdisj3b  16708  gsummptfzsplitl  16953  dmdprd  17029  subgdmdprd  17081  pgpfaclem1  17132  subrgpropd  17463  crng2idl  17887  obselocv  18759  basis1  19451  baspartn  19455  eltg  19458  tgdom  19480  indistopon  19502  ntrval  19537  clslp  19649  resttopon2  19669  restopnb  19676  paste  19795  nrmsep3  19856  imacmp  19897  cmpsub  19900  bwth  19910  llyi  19975  nllyi  19976  cldllycmp  19996  kgencmp2  20047  ptbasfi  20082  kqdisj  20233  kqcldsat  20234  trfbas2  20344  filss  20354  elfg  20372  flimclslem  20485  fcfneii  20538  tsmsfbas  20626  restutopopn  20741  ressxms  21028  restmetu  21090  qtopbaslem  21265  pi1addf  21547  pi1addval  21548  shftmbl  21949  voliunlem1  21960  voliunlem2  21961  uniioombllem2  21992  uniioombllem4  21995  uniioombllem6  21997  volsup2  22014  volcn  22015  volivth  22016  itg1climres  22121  limciun  22298  dvres3a  22318  ig1pval  22573  2pthlem2  24598  frgrancvvdeqlem4  25033  issubgo  25305  omlsi  26322  pjoml  26354  chdmj3  26449  chdmj4  26450  ledi  26458  cmbr  26502  cmbr3  26526  pjoml3  26530  fh1  26536  fh2  26537  dmdbr  27218  dmdmd  27219  dmdbr5  27227  dmdsl3  27234  chirredlem2  27310  chirredlem3  27311  dmdbr6ati  27342  disji2f  27438  disjif2  27442  disjxpin  27447  disjunsn  27453  fimacnvinrn  27475  fimacnvinrn2  27476  prsss  27898  ballotlemfval  28428  signsplypnf  28507  mvrsval  28865  msrfval  28897  mthmpps  28942  dfpo2  29184  elima4  29209  predep  29272  mblfinlem2  30052  ftc1anclem6  30095  topbnd  30142  opnbnd  30143  cldbnd  30144  neibastop1  30177  neibastop2lem  30178  neibastop2  30179  neibastop3  30180  neifg  30189  heiborlem3  30309  elrfi  30626  elrfirn  30627  elrfirn2  30628  eldioph2lem1  30693  fresin2  31448  lptioo2  31637  lptioo1  31638  cncfuni  31689  fourierdlem48  31937  fourierdlem49  31938  fourierdlem93  31982  resisresindm  32305  bnj1326  34082  bj-diagval  34605  pmodN  35574  polvalN  35629  polatN  35655  trnsetN  35881  djavalN  36862  dihmeetbclemN  37031  dihmeetlem11N  37044  djhval  37125  lclkrlem2e  37238  lcfrlem23  37292  lcdlss2N  37347  conrel2d  37762

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482