Theorem inex2 5336

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

Syntax hints:   ∈ wcel 2108  Vcvv 3488   ∩ cin 3975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-in 3983

This theorem is referenced by:  ssex  5339  wefrc  5694  hartogslem1  9611  infxpenlem  10082  dfac5lem5  10196  fin23lem12  10400  fpwwe2lem11  10710  cnso  16295  ressbas  17293  ressbasOLD  17294  ressress  17307  rescabs  17896  rescabsOLD  17897  symgvalstruct  19438  symgvalstructOLD  19439  mgpress  20176  mgpressOLD  20177  pjfval  21749  tgdom  23006  distop  23023  ustfilxp  24242  elovolmlem  25528  dyadmbl  25654  volsup2  25659  vitali  25667  itg1climres  25769  tayl0  26421  atomli  32414  ldgenpisyslem1  34127  reprinfz1  34599  bj-elid4  37134  aomclem6  43016  elinintrab  43539  isotone2  44011  ntrrn  44084  ntrf  44085  dssmapntrcls  44090  ismnushort  44270  onfrALTlem3  44515  limcresiooub  45563  limcresioolb  45564  limsupval4  45715  sge0iunmptlemre  46336  ovolval2lem  46564  ovolval4lem2  46571  setrec2fun  48784