Theorem inex2 5268

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

Syntax hints:   ∈ wcel 2109  Vcvv 3444   ∩ cin 3910

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 2701  ax-sep 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-in 3918

This theorem is referenced by:  ssex  5271  wefrc  5625  hartogslem1  9471  infxpenlem  9942  dfac5lem5  10056  fin23lem12  10260  fpwwe2lem11  10570  cnso  16191  ressbas  17182  ressress  17193  rescabs  17771  symgvalstruct  19303  mgpress  20035  pjfval  21591  tgdom  22841  distop  22858  ustfilxp  24076  elovolmlem  25351  dyadmbl  25477  volsup2  25482  vitali  25490  itg1climres  25591  tayl0  26245  atomli  32284  ldgenpisyslem1  34126  reprinfz1  34586  bj-elid4  37129  aomclem6  43021  elinintrab  43539  isotone2  44011  ntrrn  44084  ntrf  44085  dssmapntrcls  44090  ismnushort  44263  onfrALTlem3  44507  sswfaxreg  44950  limcresiooub  45613  limcresioolb  45614  limsupval4  45765  sge0iunmptlemre  46386  ovolval2lem  46614  ovolval4lem2  46621  setrec2fun  49654