Theorem inex2 4800

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

Hypothesis

Ref	Expression
inex2.1	|- A e. _V

Assertion

Ref	Expression
inex2	|- ( B i^i A ) e. _V

Proof of Theorem inex2

Step	Hyp	Ref	Expression
1		incom 3805	. 2 |- ( B i^i A ) = ( A i^i B )
2		inex2.1	. . 3 |- A e. _V
3	2	inex1 4799	. 2 |- ( A i^i B ) e. _V
4	1, 3	eqeltri 2697	1 |- ( B i^i A ) e. _V

Syntax hints:   e. wcel 1990   _Vcvv 3200   i^i cin 3573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581

This theorem is referenced by:  ssex  4802  wefrc  5108  hartogslem1  8447  infxpenlem  8836  dfac5lem5  8950  fin23lem12  9153  fpwwe2lem12  9463  cnso  14976  ressbas  15930  ressress  15938  rescabs  16493  mgpress  18500  pjfval  20050  tgdom  20782  distop  20799  ustfilxp  22016  elovolm  23243  elovolmr  23244  ovolmge0  23245  ovolgelb  23248  ovolunlem1a  23264  ovolunlem1  23265  ovoliunlem1  23270  ovoliunlem2  23271  ovolshftlem2  23278  ovolicc2  23290  ioombl1  23330  dyadmbl  23368  volsup2  23373  vitali  23382  itg1climres  23481  tayl0  24116  atomli  29241  ldgenpisyslem1  30226  reprinfz1  30700  aomclem6  37629  elinintrab  37883  isotone2  38347  ntrrn  38420  ntrf  38421  dssmapntrcls  38426  onfrALTlem3  38759  limcresiooub  39874  limcresioolb  39875  limsupval4  40026  sge0iunmptlemre  40632  ovolval2lem  40857  ovolval4lem2  40864  setrec2fun  42439