Theorem inex1g 5187

Description: Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995.)

Assertion

Ref	Expression
inex1g	⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

Proof of Theorem inex1g

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ineq1 4131	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝐵) = (𝐴 ∩ 𝐵))
2	1	eleq1d 2874	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V))
3		vex 3444	. . 3 ⊢ 𝑥 ∈ V
4	3	inex1 5185	. 2 ⊢ (𝑥 ∩ 𝐵) ∈ V
5	2, 4	vtoclg 3515	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  Vcvv 3441   ∩ cin 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-sep 5167

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-in 3888

This theorem is referenced by:  inex2g  5188  dmresexg  5842  onin  6190  offval  7396  offval3  7665  onsdominel  8650  ssenen  8675  inelfi  8866  fiin  8870  tskwe  9363  dfac8b  9442  ac10ct  9445  infpwfien  9473  fictb  9656  canthnum  10060  gruina  10229  ressinbas  16552  ressress  16554  qusin  16809  catcbas  17349  fpwipodrs  17766  psss  17816  gsumzres  19022  eltg  21562  eltg3  21567  ntrval  21641  restco  21769  restfpw  21784  ordtrest  21807  ordtrest2lem  21808  ordtrest2  21809  cnrmi  21965  restcnrm  21967  kgeni  22142  tsmsfbas  22733  eltsms  22738  tsmsres  22749  caussi  23901  causs  23902  elpwincl1  30298  disjdifprg2  30339  sigainb  31505  ldgenpisyslem1  31532  carsgclctun  31689  eulerpartlemgs2  31748  sseqval  31756  reprinrn  31999  bnj1177  32388  cvmsss2  32634  satef  32776  satefvfmla0  32778  frrlem13  33248  fnemeet2  33828  ontgval  33892  bj-discrmoore  34526  bj-ideqb  34574  bj-opelidres  34576  bj-opelidb1ALT  34581  fin2so  35044  inex3  35755  inxpex  35756  dfrefrels2  35913  dfsymrels2  35941  dftrrels2  35971  elrfi  39635  iunrelexp0  40403  fourierdlem71  42819  fourierdlem80  42828  sge0less  43031  sge0ssre  43036  carageniuncllem2  43161  dfrngc2  44596  rnghmsscmap2  44597  rngcbasALTV  44607  dfringc2  44642  rhmsscmap2  44643  rhmsscrnghm  44650  rngcresringcat  44654  ringcbasALTV  44670  srhmsubc  44700  fldc  44707  fldhmsubc  44708  rngcrescrhm  44709  srhmsubcALTV  44718  fldcALTV  44725  fldhmsubcALTV  44726  rngcrescrhmALTV  44727