Theorem inex2 5257

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

Syntax hints:   ∈ wcel 2109  Vcvv 3436   ∩ cin 3902

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 5235

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 3395  df-v 3438  df-in 3910

This theorem is referenced by:  ssex  5260  wefrc  5613  hartogslem1  9434  infxpenlem  9907  dfac5lem5  10021  fin23lem12  10225  fpwwe2lem11  10535  cnso  16156  ressbas  17147  ressress  17158  rescabs  17740  symgvalstruct  19276  mgpress  20035  pjfval  21613  tgdom  22863  distop  22880  ustfilxp  24098  elovolmlem  25373  dyadmbl  25499  volsup2  25504  vitali  25512  itg1climres  25613  tayl0  26267  atomli  32326  ldgenpisyslem1  34130  reprinfz1  34590  bj-elid4  37146  aomclem6  43036  elinintrab  43554  isotone2  44026  ntrrn  44099  ntrf  44100  dssmapntrcls  44105  ismnushort  44278  onfrALTlem3  44522  sswfaxreg  44965  limcresiooub  45627  limcresioolb  45628  limsupval4  45779  sge0iunmptlemre  46400  ovolval2lem  46628  ovolval4lem2  46635  setrec2fun  49681