Theorem inex2 5107

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

Hypothesis

Ref	Expression
inex2.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
inex2	⊢ (𝐵 ∩ 𝐴) ∈ V

Proof of Theorem inex2

Step	Hyp	Ref	Expression
1		incom 4094	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inex2.1	. . 3 ⊢ 𝐴 ∈ V
3	2	inex1 5106	. 2 ⊢ (𝐴 ∩ 𝐵) ∈ V
4	1, 3	eqeltri 2877	1 ⊢ (𝐵 ∩ 𝐴) ∈ V

Syntax hints:   ∈ wcel 2079  Vcvv 3432   ∩ cin 3853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767  ax-sep 5088

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-v 3434  df-in 3861

This theorem is referenced by:  ssex  5109  wefrc  5429  hartogslem1  8842  infxpenlem  9274  dfac5lem5  9388  fin23lem12  9588  fpwwe2lem12  9898  cnso  15421  ressbas  16371  ressress  16379  rescabs  16920  mgpress  18928  pjfval  20520  tgdom  21258  distop  21275  ustfilxp  22492  elovolmlem  23746  dyadmbl  23872  volsup2  23877  vitali  23885  itg1climres  23986  tayl0  24621  atomli  29838  ldgenpisyslem1  30995  reprinfz1  31466  aomclem6  39095  elinintrab  39373  isotone2  39835  ntrrn  39908  ntrf  39909  dssmapntrcls  39914  onfrALTlem3  40369  limcresiooub  41419  limcresioolb  41420  limsupval4  41571  sge0iunmptlemre  42193  ovolval2lem  42421  ovolval4lem2  42428  setrec2fun  44229