Theorem ineq2 3693

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

Assertion

Ref	Expression
ineq2

Proof of Theorem ineq2

Step	Hyp	Ref	Expression
1		ineq1 3692	. 2
2		incom 3690	. 2
3		incom 3690	. 2
4	1, 2, 3	3eqtr4g 2523	1

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

This theorem is referenced by:  ineq12  3694  ineq2i  3696  ineq2d  3699  uneqin  3748  intprg  4321  wefrc  4878  onfr  4922  onnseq  7034  qsdisj  7407  disjenex  7695  fiint  7817  elfiun  7910  dffi3  7911  cplem2  8329  dfac5  8530  kmlem2  8552  kmlem13  8563  kmlem14  8564  ackbij1lem16  8636  fin23lem12  8732  fin23lem19  8737  fin23lem33  8746  uzin2  13177  pgpfac1lem3  17128  pgpfac1lem5  17130  pgpfac1  17131  inopn  19408  basis1  19451  basis2  19452  baspartn  19455  fctop  19505  cctop  19507  ordtbaslem  19689  hausnei2  19854  cnhaus  19855  nrmsep  19858  isnrm2  19859  dishaus  19883  ordthauslem  19884  bwthOLD  19911  dfcon2  19920  nconsubb  19924  finlocfin  20021  dissnlocfin  20030  locfindis  20031  kgeni  20038  pthaus  20139  txhaus  20148  xkohaus  20154  regr1lem  20240  fbasssin  20337  fbun  20341  fbunfip  20370  filcon  20384  isufil2  20409  ufileu  20420  filufint  20421  fmfnfmlem4  20458  fmfnfm  20459  fclsopni  20516  fclsbas  20522  fclsrest  20525  isfcf  20535  tsmsfbas  20626  ustincl  20710  ust0  20722  metreslem  20865  methaus  21023  qtopbaslem  21265  metnrmlem3  21365  ismbl  21937  shincl  26299  chincl  26417  chdmm1  26443  ledi  26458  cmbr  26502  cmbr3i  26518  cmbr3  26526  pjoml2  26529  stcltrlem1  27195  mdbr  27213  dmdbr  27218  cvmd  27255  cvexch  27293  sumdmdii  27334  mddmdin0i  27350  ofpreima2  27508  crefeq  27848  ballotlemfval  28428  ballotlemgval  28462  cvmscbv  28703  cvmsdisj  28715  cvmsss2  28719  nepss  29095  mblfinlem2  30052  tailfb  30195  elrfi  30626  fouriersw  32014  csbresgVD  33695  lshpinN  34714  fipjust  37750  conrel1d  37761

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