Theorem inex2 5298

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 4189	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		inex2.1	. . 3 ⊢ 𝐴 ∈ V
3	2	inex1 5297	. 2 ⊢ (𝐴 ∩ 𝐵) ∈ V
4	1, 3	eqeltri 2829	1 ⊢ (𝐵 ∩ 𝐴) ∈ V

Syntax hints:   ∈ wcel 2107  Vcvv 3463   ∩ cin 3930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-sep 5276

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420  df-v 3465  df-in 3938

This theorem is referenced by:  ssex  5301  wefrc  5659  hartogslem1  9564  infxpenlem  10035  dfac5lem5  10149  fin23lem12  10353  fpwwe2lem11  10663  cnso  16266  ressbas  17259  ressbasOLD  17260  ressress  17271  rescabs  17849  rescabsOLD  17850  symgvalstruct  19383  symgvalstructOLD  19384  mgpress  20116  pjfval  21681  tgdom  22933  distop  22950  ustfilxp  24168  elovolmlem  25446  dyadmbl  25572  volsup2  25577  vitali  25585  itg1climres  25686  tayl0  26340  atomli  32330  ldgenpisyslem1  34139  reprinfz1  34612  bj-elid4  37144  aomclem6  43049  elinintrab  43567  isotone2  44039  ntrrn  44112  ntrf  44113  dssmapntrcls  44118  ismnushort  44292  onfrALTlem3  44536  sswfaxreg  44976  limcresiooub  45629  limcresioolb  45630  limsupval4  45781  sge0iunmptlemre  46402  ovolval2lem  46630  ovolval4lem2  46637  setrec2fun  49306