Theorem inex2 5246

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

Syntax hints:   ∈ wcel 2119  Vcvv 3431   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-in 3890

This theorem is referenced by:  ssex  5249  wefrc  5612  hartogslem1  9447  infxpenlem  9926  dfac5lem5  10040  fin23lem12  10244  fpwwe2lem11  10555  cnso  16205  ressbas  17197  ressress  17208  rescabs  17791  symgvalstruct  19363  mgpress  20122  pjfval  21681  tgdom  22961  distop  22978  ustfilxp  24196  elovolmlem  25459  dyadmbl  25585  volsup2  25590  vitali  25598  itg1climres  25699  tayl0  26345  atomli  32471  ldgenpisyslem1  34347  reprinfz1  34806  dfttc4  36758  bj-elid4  37528  aomclem6  43504  elinintrab  44021  isotone2  44493  ntrrn  44566  ntrf  44567  dssmapntrcls  44572  ismnushort  44745  onfrALTlem3  44988  sswfaxreg  45431  limcresiooub  46085  limcresioolb  46086  limsupval4  46237  sge0iunmptlemre  46858  ovolval2lem  47086  ovolval4lem2  47093  nthrucw  47331  setrec2fun  50182