Theorem ineq1i 3695

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

Hypothesis

Ref	Expression
ineq1i.1

Assertion

Ref	Expression
ineq1i

Proof of Theorem ineq1i

Step	Hyp	Ref	Expression
1		ineq1i.1	. 2
2		ineq1 3692	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  =wceq 1395  i^icin 3474

This theorem is referenced by:  in12  3708  inindi  3714  dfrab3  3772  dfif5  3957  disjpr2  4092  resres  5291  imainrect  5453  fresaun  5761  fresaunres2  5762  ssenen  7711  hartogslem1  7988  leiso  12508  f1oun2prg  12865  smumul  14143  firest  14830  lsmdisj2r  16703  frgpuplem  16790  ltbwe  18137  tgrest  19660  fiuncmp  19904  ptclsg  20116  metnrmlem3  21365  mbfid  22043  ppi1  23438  cht1  23439  ppiub  23479  cusgrasizeindslem2  24474  chdmj2i  26400  chjassi  26404  pjoml2i  26503  pjoml4i  26505  cmcmlem  26509  mayetes3i  26648  cvmdi  27243  atomli  27301  atabsi  27320  imadifxp  27458  gtiso  27519  prsss  27898  ordtrest2NEW  27905  esumnul  28059  measinblem  28191  eulerpartlemt  28310  ballotlem2  28427  ballotlemfp1  28430  ballotlemfval0  28434  mthmpps  28942  predidm  29268  dffv5  29574  mblfinlem2  30052  ismblfin  30055  mbfposadd  30062  itg2addnclem2  30067  asindmre  30102  diophrw  30692  dnwech  30994  lmhmlnmsplit  31033  nznngen  31221  rp-fakeuninass  37741

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