Theorem ineq1d 3698

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

Step	Hyp	Ref	Expression
1		ineq1d.1	. 2
2		ineq1 3692	. 2
3	1, 2	syl 16	1

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

This theorem is referenced by:  diftpsn3  4168  iinrab2  4393  disji2  4439  disjprg  4448  disjxun  4450  riinint  5264  fnresdisj  5696  fnimadisj  5706  fninfp  6098  ecinxp  7405  fiint  7817  fival  7892  marypha1lem  7913  kmlem12  8562  fin23lem12  8732  fin23lem30  8743  fin23lem33  8746  ttukeylem1  8910  fpwwe2cbv  9029  fpwwe2lem2  9031  fpwwe2  9042  fzval2  11704  injresinjlem  11925  limsupval  13297  limsupgval  13299  ello1  13338  elo1  13349  fsum1p  13568  incexclem  13648  fprod1p  13772  smuval2  14132  smueqlem  14140  smumul  14143  isacs2  15050  acsfiel  15051  isacs1i  15054  catcval  15423  resscatc  15432  acsficl  15801  lsmdisj3  16701  lsmdisj3a  16707  dprdres  17075  dprdz  17077  dpjdisj  17102  lspdisj2  17773  indistopon  19502  restopnb  19676  ordtrest2  19705  isnrm  19836  cmpcov  19889  cmpsublem  19899  cmpsub  19900  tgcmp  19901  uncmp  19903  hauscmplem  19906  bwthOLD  19911  nconsubb  19924  isnlly  19970  dissnlocfin  20030  kgeni  20038  kgencn3  20059  ptcld  20114  ptcnplem  20122  alexsublem  20544  alexsubb  20546  alexsubALTlem2  20548  alexsubALTlem4  20550  alexsubALT  20551  tmdgsum2  20595  tsmsval2  20628  ustexsym  20718  metrest  21027  qtopbaslem  21265  cnheibor  21455  bndth  21458  lebnumii  21466  iscph  21617  csscld  21689  clsocv  21690  ovolicc2  21933  voliunlem3  21962  ioombl  21975  uniioombllem2  21992  uniioombllem4  21995  uniioombllem6  21997  mbflimsup  22073  taylfval  22754  chtval  23384  ppival  23401  ppival2  23402  ppival2g  23403  chtfl  23423  ppiprm  23425  chtprm  23427  chtnprm  23428  chtdif  23432  ppidif  23437  prmorcht  23452  2pthlem2  24598  frgrancvvdeqlem4  25033  chdmj2  26448  cmcmlem  26509  pjoml2  26529  fh2  26537  mdbr  27213  mdi  27214  mdbr3  27216  mdbr4  27217  dmdmd  27219  dmdbr3  27224  dmdbr4  27225  dmdi4  27226  dmdbr5  27227  mddmd2  27228  mdsl1i  27240  cvmdi  27243  mdslmd1lem1  27244  mdslmd1lem2  27245  mdslmd1lem3  27246  mdslmd1lem4  27247  mdslmd1i  27248  mdslmd3i  27251  csmdsymi  27253  mdexchi  27254  atomli  27301  atabsi  27320  sumdmdlem2  27338  dmdbr5ati  27341  disji2f  27438  disjif2  27442  disjxpin  27447  disjunsn  27453  fnresin  27470  locfinreflem  27843  iscref  27847  ordtrest2NEW  27905  ordtconlem1  27906  totprobd  28365  probmeasb  28369  ballotlemfval  28428  ballotlemfp1  28430  ballotlemgun  28463  iccllyscon  28695  mvrsval  28865  mrsubvrs  28882  mpstval  28895  msubvrs  28920  limsucncmpi  29910  ptrest  30048  mblfinlem2  30052  neibastop2lem  30178  neibastop2  30179  neibastop3  30180  sstotbnd2  30270  cntotbnd  30292  heibor  30317  elrfi  30626  isnacs  30636  mrefg2  30639  mapfzcons2  30651  coeq0i  30686  eldioph2lem2  30694  aomclem8  31007  kelac1  31009  islmodfg  31015  lnr2i  31065  fgraphopab  31170  lptre2pt  31646  stoweidlem50  31832  stoweidlem57  31839  aacllem  33216  bnj1385  33891  bnj1326  34082  l1cvat  34780  pmodlem2  35571  pmod2iN  35573  hlmod1i  35580  osumcllem3N  35682  osumcllem9N  35688  pexmidlem6N  35699  pl42lem1N  35703  istrnN  35882  djavalN  36862  dihmeetlem9N  37042  dihmeetlem11N  37044  dihmeetlem12N  37045  dihoml4  37104  djhval  37125  dochexmidlem6  37192  lclkrlem2b  37235  lcfrlem20  37289  lcfrlem23  37292

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