Theorem inex2 5323

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

Syntax hints:   ∈ wcel 2099  Vcvv 3462   ∩ cin 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-sep 5304

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-v 3464  df-in 3954

This theorem is referenced by:  ssex  5326  wefrc  5676  hartogslem1  9585  infxpenlem  10056  dfac5lem5  10170  fin23lem12  10374  fpwwe2lem11  10684  cnso  16249  ressbas  17248  ressbasOLD  17249  ressress  17262  rescabs  17851  rescabsOLD  17852  symgvalstruct  19394  symgvalstructOLD  19395  mgpress  20132  mgpressOLD  20133  pjfval  21704  tgdom  22972  distop  22989  ustfilxp  24208  elovolmlem  25494  dyadmbl  25620  volsup2  25625  vitali  25633  itg1climres  25735  tayl0  26389  atomli  32315  ldgenpisyslem1  33996  reprinfz1  34468  bj-elid4  36875  aomclem6  42720  elinintrab  43244  isotone2  43716  ntrrn  43789  ntrf  43790  dssmapntrcls  43795  ismnushort  43975  onfrALTlem3  44220  limcresiooub  45263  limcresioolb  45264  limsupval4  45415  sge0iunmptlemre  46036  ovolval2lem  46264  ovolval4lem2  46271  setrec2fun  48438