Theorem inex2 4952

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

Syntax hints:   ∈ wcel 2139  Vcvv 3340   ∩ cin 3714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-in 3722

This theorem is referenced by:  ssex  4954  wefrc  5260  hartogslem1  8614  infxpenlem  9046  dfac5lem5  9160  fin23lem12  9365  fpwwe2lem12  9675  cnso  15195  ressbas  16152  ressress  16160  rescabs  16714  mgpress  18720  pjfval  20272  tgdom  21004  distop  21021  ustfilxp  22237  elovolm  23463  elovolmr  23464  ovolmge0  23465  ovolgelb  23468  ovolunlem1a  23484  ovolunlem1  23485  ovoliunlem1  23490  ovoliunlem2  23491  ovolshftlem2  23498  ovolicc2  23510  ioombl1  23550  dyadmbl  23588  volsup2  23593  vitali  23601  itg1climres  23700  tayl0  24335  atomli  29571  ldgenpisyslem1  30556  reprinfz1  31030  aomclem6  38149  elinintrab  38403  isotone2  38867  ntrrn  38940  ntrf  38941  dssmapntrcls  38946  onfrALTlem3  39279  limcresiooub  40395  limcresioolb  40396  limsupval4  40547  sge0iunmptlemre  41153  ovolval2lem  41381  ovolval4lem2  41388  setrec2fun  42967