Theorem inex2 5261

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

Syntax hints:   ∈ wcel 2113  Vcvv 3438   ∩ cin 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-in 3906

This theorem is referenced by:  ssex  5264  wefrc  5616  hartogslem1  9445  infxpenlem  9921  dfac5lem5  10035  fin23lem12  10239  fpwwe2lem11  10550  cnso  16170  ressbas  17161  ressress  17172  rescabs  17755  symgvalstruct  19324  mgpress  20083  pjfval  21659  tgdom  22920  distop  22937  ustfilxp  24155  elovolmlem  25429  dyadmbl  25555  volsup2  25560  vitali  25568  itg1climres  25669  tayl0  26323  atomli  32406  ldgenpisyslem1  34269  reprinfz1  34728  bj-elid4  37312  aomclem6  43243  elinintrab  43760  isotone2  44232  ntrrn  44305  ntrf  44306  dssmapntrcls  44311  ismnushort  44484  onfrALTlem3  44727  sswfaxreg  45170  limcresiooub  45828  limcresioolb  45829  limsupval4  45980  sge0iunmptlemre  46601  ovolval2lem  46829  ovolval4lem2  46836  nthrucw  47072  setrec2fun  49879