Theorem ineq2i 3696

Description: Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.)

Hypothesis

Ref	Expression
ineq1i.1

Assertion

Ref	Expression
ineq2i

Proof of Theorem ineq2i

Step	Hyp	Ref	Expression
1		ineq1i.1	. 2
2		ineq2 3693	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  =wceq 1395  i^icin 3474

This theorem is referenced by:  in4  3713  inindir  3715  indif2  3740  difun1  3757  dfrab3ss  3775  undif1  3903  difdifdir  3915  dfif3  3955  dfif5  3957  intunsn  4326  rint0  4327  riin0  4404  csbres  5281  res0  5283  resres  5291  resundi  5292  resindi  5294  inres  5296  resiun2  5298  resopab  5325  dffr3  5374  dfse2  5375  dminxp  5452  imainrect  5453  resdmres  5503  funimacnv  5665  fresaun  5761  fresaunres2  5762  tfrlem10  7075  sbthlem5  7651  infssuni  7831  dfsup2  7922  dfsup2OLD  7923  dfsup3OLD  7924  en3lplem2  8053  wemapwe  8160  wemapweOLD  8161  epfrs  8183  r0weon  8411  infxpenlem  8412  kmlem11  8561  ackbij1lem1  8621  ackbij1lem2  8622  axdc3lem4  8854  canthwelem  9049  dmaddpi  9289  dmmulpi  9290  ssxr  9675  dmhashres  12414  fz1isolem  12510  f1oun2prg  12865  fsumiun  13635  sadeq  14122  bitsres  14123  smuval2  14132  smumul  14143  ressinbas  14693  lubdm  15609  glbdm  15622  sylow2a  16639  lsmmod2  16694  lsmdisj2r  16703  ablfac1eu  17124  ressmplbas2  18117  opsrtoslem1  18148  pjdm  18738  rintopn  19418  ordtrest2  19705  cmpsublem  19899  bwthOLD  19911  kgentopon  20039  hausdiag  20146  uzrest  20398  ufprim  20410  trust  20732  metnrmlem3  21365  clsocv  21690  ismbl  21937  unmbl  21948  volinun  21956  voliunlem1  21960  ovolioo  21978  itg2cnlem2  22169  ellimc2  22281  limcflf  22285  lhop1lem  22414  lgsquadlem3  23631  rplogsum  23712  0pth  24572  1pthonlem2  24592  frgrancvvdeqlem4  25033  ex-in  25146  chdmj3i  26401  chdmj4i  26402  chjassi  26404  pjoml2i  26503  pjoml3i  26504  cmcmlem  26509  cmcm2i  26511  cmbr3i  26518  fh3i  26541  fh4i  26542  osumcor2i  26562  mayetes3i  26648  mdslmd3i  27251  mdexchi  27254  atabsi  27320  dmdbr5ati  27341  inin  27413  ordtrest2NEW  27905  hasheuni  28091  eulerpartgbij  28311  fiblem  28337  cvmscld  28718  msrid  28905  dfpo2  29184  elrn3  29192  dfpred2  29253  predidm  29268  wfrlem13  29355  mblfinlem2  30052  ftc1anclem6  30095  mapfzcons2  30651  diophrw  30692  hashnzfz  31225  fourierdlem80  31969  pol0N  35633  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