Theorem inex1g 5288

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 4166	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝐵) = (𝐴 ∩ 𝐵))
2	1	eleq1d 2848	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V))
3		vex 3459	. . 3 ⊢ 𝑥 ∈ V
4	3	inex1 5286	. 2 ⊢ (𝑥 ∩ 𝐵) ∈ V
5	2, 4	vtoclg 3522	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  Vcvv 3455   ∩ cin 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-in 3912

This theorem is referenced by:  inex2g  5289  dmresexg  6013  predexg  6320  onin  6392  offval  7683  offval3  7975  frrlem13  8291  onsdominel  9110  ssenen  9135  inelfi  9374  fiin  9378  tskwe  9932  dfac8b  10011  ac10ct  10014  infpwfien  10042  fictb  10223  canthnum  10629  gruina  10798  ressinbas  17300  ressress  17302  qusin  17593  catcbas  18153  fpwipodrs  18591  psss  18631  gsumzres  19974  dfrngc2  20727  rnghmsscmap2  20728  dfringc2  20756  rhmsscmap2  20757  rhmsscrnghm  20764  rngcresringcat  20768  srhmsubc  20779  rngcrescrhm  20783  fldc  20887  fldhmsubc  20888  eltg  23114  eltg3  23119  ntrval  23193  restco  23321  restfpw  23336  ordtrest  23359  ordtrest2lem  23360  ordtrest2  23361  cnrmi  23517  restcnrm  23519  kgeni  23694  tsmsfbas  24285  eltsms  24290  tsmsres  24301  caussi  25456  causs  25457  elpwincl1  32871  disjdifprg2  32921  sigainb  34526  ldgenpisyslem1  34553  carsgclctun  34711  eulerpartlemgs2  34770  sseqval  34778  reprinrn  35005  bnj1177  35394  cvmsss2  35766  satef  35908  satefvfmla0  35910  fnemeet2  36898  ontgval  36962  bj-discrmoore  37773  bj-ideqb  37823  bj-opelidres  37825  bj-opelidb1ALT  37830  fin2so  38278  inex3  39007  inxpex  39008  dfrefrels2  39262  dfsymrels2  39294  dftrrels2  39328  elrfi  43445  ofoafg  44101  fourierdlem71  46911  fourierdlem80  46920  sge0less  47126  sge0ssre  47131  carageniuncllem2  47256  rngcbasALTV  49051  rngcrescrhmALTV  49065  ringcbasALTV  49085  srhmsubcALTV  49110  fldcALTV  49117  fldhmsubcALTV  49118