Theorem inex2 5273

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

Syntax hints:   ∈ wcel 2109  Vcvv 3447   ∩ cin 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-in 3921

This theorem is referenced by:  ssex  5276  wefrc  5632  hartogslem1  9495  infxpenlem  9966  dfac5lem5  10080  fin23lem12  10284  fpwwe2lem11  10594  cnso  16215  ressbas  17206  ressress  17217  rescabs  17795  symgvalstruct  19327  mgpress  20059  pjfval  21615  tgdom  22865  distop  22882  ustfilxp  24100  elovolmlem  25375  dyadmbl  25501  volsup2  25506  vitali  25514  itg1climres  25615  tayl0  26269  atomli  32311  ldgenpisyslem1  34153  reprinfz1  34613  bj-elid4  37156  aomclem6  43048  elinintrab  43566  isotone2  44038  ntrrn  44111  ntrf  44112  dssmapntrcls  44117  ismnushort  44290  onfrALTlem3  44534  sswfaxreg  44977  limcresiooub  45640  limcresioolb  45641  limsupval4  45792  sge0iunmptlemre  46413  ovolval2lem  46641  ovolval4lem2  46648  setrec2fun  49681