Theorem inex2 5280

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

Syntax hints:   ∈ wcel 2106  Vcvv 3446   ∩ cin 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-in 3920

This theorem is referenced by:  ssex  5283  wefrc  5632  hartogslem1  9487  infxpenlem  9958  dfac5lem5  10072  fin23lem12  10276  fpwwe2lem11  10586  cnso  16140  ressbas  17129  ressbasOLD  17130  ressress  17143  rescabs  17732  rescabsOLD  17733  symgvalstruct  19192  symgvalstructOLD  19193  mgpress  19925  mgpressOLD  19926  pjfval  21149  tgdom  22365  distop  22382  ustfilxp  23601  elovolmlem  24875  dyadmbl  25001  volsup2  25006  vitali  25014  itg1climres  25116  tayl0  25758  atomli  31387  ldgenpisyslem1  32851  reprinfz1  33324  bj-elid4  35712  aomclem6  41444  elinintrab  41971  isotone2  42443  ntrrn  42516  ntrf  42517  dssmapntrcls  42522  ismnushort  42703  onfrALTlem3  42948  limcresiooub  44003  limcresioolb  44004  limsupval4  44155  sge0iunmptlemre  44776  ovolval2lem  45004  ovolval4lem2  45011  setrec2fun  47257