Theorem inex2 5287

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

Syntax hints:   ∈ wcel 2143  Vcvv 3455   ∩ cin 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-in 3912

This theorem is referenced by:  ssexOLD  5292  wefrc  5655  hartogslem1  9500  infxpenlem  9993  dfac5lem5  10107  fin23lem12  10310  fpwwe2lem11  10621  cnso  16298  ressbas  17291  ressress  17302  rescabs  17885  symgvalstruct  19462  mgpress  20221  pjfval  21856  tgdom  23135  distop  23152  ustfilxp  24370  elovolmlem  25633  dyadmbl  25759  volsup2  25764  vitali  25772  itg1climres  25873  tayl0  26525  atomli  32734  ldgenpisyslem1  34553  reprinfz1  35009  dfttc4  37061  bj-elid4  37832  aomclem6  43806  elinintrab  44323  isotone2  44795  ntrrn  44868  ntrf  44869  dssmapntrcls  44874  ismnushort  45031  onfrALTlem3  45273  sswfaxreg  45716  limcresiooub  46376  limcresioolb  46377  limsupval4  46528  sge0iunmptlemre  47149  ovolval2lem  47377  ovolval4lem2  47384  nthrucw  47627  setrec2fun  50490