Theorem inex2 4950

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

Syntax hints:   ∈ wcel 2137  Vcvv 3338   ∩ cin 3712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-sep 4931

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-v 3340  df-in 3720

This theorem is referenced by:  ssex  4952  wefrc  5258  hartogslem1  8610  infxpenlem  9024  dfac5lem5  9138  fin23lem12  9343  fpwwe2lem12  9653  cnso  15173  ressbas  16130  ressress  16138  rescabs  16692  mgpress  18698  pjfval  20250  tgdom  20982  distop  20999  ustfilxp  22215  elovolm  23441  elovolmr  23442  ovolmge0  23443  ovolgelb  23446  ovolunlem1a  23462  ovolunlem1  23463  ovoliunlem1  23468  ovoliunlem2  23469  ovolshftlem2  23476  ovolicc2  23488  ioombl1  23528  dyadmbl  23566  volsup2  23571  vitali  23579  itg1climres  23678  tayl0  24313  atomli  29548  ldgenpisyslem1  30533  reprinfz1  31007  aomclem6  38129  elinintrab  38383  isotone2  38847  ntrrn  38920  ntrf  38921  dssmapntrcls  38926  onfrALTlem3  39259  limcresiooub  40375  limcresioolb  40376  limsupval4  40527  sge0iunmptlemre  41133  ovolval2lem  41361  ovolval4lem2  41368  setrec2fun  42947