Theorem inex2 5224

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

Syntax hints:   ∈ wcel 2114  Vcvv 3496   ∩ cin 3937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-in 3945

This theorem is referenced by:  ssex  5227  wefrc  5551  hartogslem1  9008  infxpenlem  9441  dfac5lem5  9555  fin23lem12  9755  fpwwe2lem12  10065  cnso  15602  ressbas  16556  ressress  16564  rescabs  17105  symgvalstruct  18527  mgpress  19252  pjfval  20852  tgdom  21588  distop  21605  ustfilxp  22823  elovolmlem  24077  dyadmbl  24203  volsup2  24208  vitali  24216  itg1climres  24317  tayl0  24952  atomli  30161  ldgenpisyslem1  31424  reprinfz1  31895  bj-elid4  34462  aomclem6  39666  elinintrab  39944  isotone2  40406  ntrrn  40479  ntrf  40480  dssmapntrcls  40485  onfrALTlem3  40885  limcresiooub  41930  limcresioolb  41931  limsupval4  42082  sge0iunmptlemre  42704  ovolval2lem  42932  ovolval4lem2  42939  setrec2fun  44802