Theorem inex2 4594

Description: Separation Scheme (Aussonderung) using class notation. (Contributed by NM, 27-Apr-1994.)

Hypothesis

Ref	Expression
inex2.1

Assertion

Ref	Expression
inex2

Proof of Theorem inex2

Step	Hyp	Ref	Expression
1		incom 3690	. 2
2		inex2.1	. . 3
3	2	inex1 4593	. 2
4	1, 3	eqeltri 2541	1

Syntax hints:  e.wcel 1818  cvv 3109  i^icin 3474

This theorem is referenced by:  ssex  4596  wefrc  4878  hartogslem1  7988  infxpenlem  8412  dfac5lem5  8529  fin23lem12  8732  fpwwe2lem12  9040  cnso  13980  ressbas  14687  ressress  14694  rescabs  15202  mgpress  17152  pjfval  18737  tgdom  19480  distop  19497  ustfilxp  20715  elovolm  21886  elovolmr  21887  ovolmge0  21888  ovolgelb  21891  ovolunlem1a  21907  ovolunlem1  21908  ovoliunlem1  21913  ovoliunlem2  21914  ovolshftlem2  21921  ovolicc2  21933  ioombl1  21972  dyadmbl  22009  volsup2  22014  vitali  22022  itg1climres  22121  tayl0  22757  atomli  27301  aomclem6  31005  limcresiooub  31648  limcresioolb  31649  onfrALTlem3  33316

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  ax-sep 4573

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