Theorem inex2 5276

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

Syntax hints:   ∈ wcel 2109  Vcvv 3450   ∩ cin 3916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-in 3924

This theorem is referenced by:  ssex  5279  wefrc  5635  hartogslem1  9502  infxpenlem  9973  dfac5lem5  10087  fin23lem12  10291  fpwwe2lem11  10601  cnso  16222  ressbas  17213  ressress  17224  rescabs  17802  symgvalstruct  19334  mgpress  20066  pjfval  21622  tgdom  22872  distop  22889  ustfilxp  24107  elovolmlem  25382  dyadmbl  25508  volsup2  25513  vitali  25521  itg1climres  25622  tayl0  26276  atomli  32318  ldgenpisyslem1  34160  reprinfz1  34620  bj-elid4  37163  aomclem6  43055  elinintrab  43573  isotone2  44045  ntrrn  44118  ntrf  44119  dssmapntrcls  44124  ismnushort  44297  onfrALTlem3  44541  sswfaxreg  44984  limcresiooub  45647  limcresioolb  45648  limsupval4  45799  sge0iunmptlemre  46420  ovolval2lem  46648  ovolval4lem2  46655  setrec2fun  49685