Theorem inex2 5259

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

Syntax hints:   ∈ wcel 2114  Vcvv 3429   ∩ cin 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-in 3896

This theorem is referenced by:  ssex  5262  wefrc  5625  hartogslem1  9457  infxpenlem  9935  dfac5lem5  10049  fin23lem12  10253  fpwwe2lem11  10564  cnso  16214  ressbas  17206  ressress  17217  rescabs  17800  symgvalstruct  19372  mgpress  20131  pjfval  21686  tgdom  22943  distop  22960  ustfilxp  24178  elovolmlem  25441  dyadmbl  25567  volsup2  25572  vitali  25580  itg1climres  25681  tayl0  26327  atomli  32453  ldgenpisyslem1  34307  reprinfz1  34766  dfttc4  36712  bj-elid4  37482  aomclem6  43487  elinintrab  44004  isotone2  44476  ntrrn  44549  ntrf  44550  dssmapntrcls  44555  ismnushort  44728  onfrALTlem3  44971  sswfaxreg  45414  limcresiooub  46070  limcresioolb  46071  limsupval4  46222  sge0iunmptlemre  46843  ovolval2lem  47071  ovolval4lem2  47078  nthrucw  47316  setrec2fun  50167