Theorem inex2 5263

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

Syntax hints:   ∈ wcel 2113  Vcvv 3440   ∩ cin 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-in 3908

This theorem is referenced by:  ssex  5266  wefrc  5618  hartogslem1  9447  infxpenlem  9923  dfac5lem5  10037  fin23lem12  10241  fpwwe2lem11  10552  cnso  16172  ressbas  17163  ressress  17174  rescabs  17757  symgvalstruct  19326  mgpress  20085  pjfval  21661  tgdom  22922  distop  22939  ustfilxp  24157  elovolmlem  25431  dyadmbl  25557  volsup2  25562  vitali  25570  itg1climres  25671  tayl0  26325  atomli  32457  ldgenpisyslem1  34320  reprinfz1  34779  bj-elid4  37373  aomclem6  43311  elinintrab  43828  isotone2  44300  ntrrn  44373  ntrf  44374  dssmapntrcls  44379  ismnushort  44552  onfrALTlem3  44795  sswfaxreg  45238  limcresiooub  45896  limcresioolb  45897  limsupval4  46048  sge0iunmptlemre  46669  ovolval2lem  46897  ovolval4lem2  46904  nthrucw  47140  setrec2fun  49947