Theorem inex2 5318

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

Syntax hints:   ∈ wcel 2108  Vcvv 3480   ∩ cin 3950

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-in 3958

This theorem is referenced by:  ssex  5321  wefrc  5679  hartogslem1  9582  infxpenlem  10053  dfac5lem5  10167  fin23lem12  10371  fpwwe2lem11  10681  cnso  16283  ressbas  17280  ressbasOLD  17281  ressress  17293  rescabs  17877  rescabsOLD  17878  symgvalstruct  19414  symgvalstructOLD  19415  mgpress  20147  pjfval  21726  tgdom  22985  distop  23002  ustfilxp  24221  elovolmlem  25509  dyadmbl  25635  volsup2  25640  vitali  25648  itg1climres  25749  tayl0  26403  atomli  32401  ldgenpisyslem1  34164  reprinfz1  34637  bj-elid4  37169  aomclem6  43071  elinintrab  43590  isotone2  44062  ntrrn  44135  ntrf  44136  dssmapntrcls  44141  ismnushort  44320  onfrALTlem3  44564  sswfaxreg  45004  limcresiooub  45657  limcresioolb  45658  limsupval4  45809  sge0iunmptlemre  46430  ovolval2lem  46658  ovolval4lem2  46665  setrec2fun  49211