Theorem inex2 5324

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

Syntax hints:   ∈ wcel 2106  Vcvv 3478   ∩ cin 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-in 3970

This theorem is referenced by:  ssex  5327  wefrc  5683  hartogslem1  9580  infxpenlem  10051  dfac5lem5  10165  fin23lem12  10369  fpwwe2lem11  10679  cnso  16280  ressbas  17280  ressbasOLD  17281  ressress  17294  rescabs  17883  rescabsOLD  17884  symgvalstruct  19429  symgvalstructOLD  19430  mgpress  20167  mgpressOLD  20168  pjfval  21744  tgdom  23001  distop  23018  ustfilxp  24237  elovolmlem  25523  dyadmbl  25649  volsup2  25654  vitali  25662  itg1climres  25764  tayl0  26418  atomli  32411  ldgenpisyslem1  34144  reprinfz1  34616  bj-elid4  37151  aomclem6  43048  elinintrab  43567  isotone2  44039  ntrrn  44112  ntrf  44113  dssmapntrcls  44118  ismnushort  44297  onfrALTlem3  44542  limcresiooub  45598  limcresioolb  45599  limsupval4  45750  sge0iunmptlemre  46371  ovolval2lem  46599  ovolval4lem2  46606  setrec2fun  48923