Theorem inex2 5274

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

Syntax hints:   ∈ wcel 2142  Vcvv 3454   ∩ cin 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-in 3911

This theorem is referenced by:  ssex  5277  wefrc  5641  hartogslem1  9490  infxpenlem  9969  dfac5lem5  10083  fin23lem12  10288  fpwwe2lem11  10599  cnso  16279  ressbas  17272  ressress  17283  rescabs  17866  symgvalstruct  19437  mgpress  20196  pjfval  21758  tgdom  23038  distop  23055  ustfilxp  24273  elovolmlem  25536  dyadmbl  25662  volsup2  25667  vitali  25675  itg1climres  25776  tayl0  26425  atomli  32585  ldgenpisyslem1  34460  reprinfz1  34916  dfttc4  36890  bj-elid4  37660  aomclem6  43636  elinintrab  44153  isotone2  44625  ntrrn  44698  ntrf  44699  dssmapntrcls  44704  ismnushort  44877  onfrALTlem3  45120  sswfaxreg  45563  limcresiooub  46216  limcresioolb  46217  limsupval4  46368  sge0iunmptlemre  46989  ovolval2lem  47217  ovolval4lem2  47224  nthrucw  47462  setrec2fun  50313