Theorem inex2 4728

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

Syntax hints:   ∈ wcel 1977  Vcvv 3173   ∩ cin 3539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547

This theorem is referenced by:  ssex  4730  wefrc  5032  hartogslem1  8330  infxpenlem  8719  dfac5lem5  8833  fin23lem12  9036  fpwwe2lem12  9342  cnso  14815  ressbas  15757  ressress  15765  rescabs  16316  mgpress  18323  pjfval  19869  tgdom  20593  distop  20610  ustfilxp  21826  elovolm  23050  elovolmr  23051  ovolmge0  23052  ovolgelb  23055  ovolunlem1a  23071  ovolunlem1  23072  ovoliunlem1  23077  ovoliunlem2  23078  ovolshftlem2  23085  ovolicc2  23097  ioombl1  23137  dyadmbl  23174  volsup2  23179  vitali  23188  itg1climres  23287  tayl0  23920  atomli  28625  ldgenpisyslem1  29553  aomclem6  36647  elinintrab  36902  isotone2  37367  ntrrn  37440  ntrf  37441  dssmapntrcls  37446  onfrALTlem3  37780  limcresiooub  38709  limcresioolb  38710  sge0iunmptlemre  39308  ovolval2lem  39533  ovolval4lem2  39540  setrec2fun  42238