Theorem inex1g 5287

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 4165	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝐵) = (𝐴 ∩ 𝐵))
2	1	eleq1d 2847	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V))
3		vex 3458	. . 3 ⊢ 𝑥 ∈ V
4	3	inex1 5285	. 2 ⊢ (𝑥 ∩ 𝐵) ∈ V
5	2, 4	vtoclg 3521	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2142  Vcvv 3454   ∩ cin 3903

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-in 3911

This theorem is used by:  inex2g  5288  dmresexg  6012  predexg  6320  onin  6392  offval  7685  offval3  7977  frrlem13  8293  onsdominel  9112  ssenen  9137  inelfi  9376  fiin  9380  tskwe  9943  infpwfien  10053  fictb  10234  canthnum  10640  gruina  10809  ressinbas  17311  ressress  17313  qusin  17604  catcbas  18164  fpwipodrs  18602  psss  18642  gsumzres  19985  dfrngc2  20738  rnghmsscmap2  20739  dfringc2  20767  rhmsscmap2  20768  rhmsscrnghm  20775  rngcresringcat  20779  srhmsubc  20790  rngcrescrhm  20794  fldc  20898  fldhmsubc  20899  eltg  23125  eltg3  23130  ntrval  23204  restco  23332  restfpw  23347  ordtrest  23370  ordtrest2lem  23371  ordtrest2  23372  cnrmi  23528  restcnrm  23530  kgeni  23705  tsmsfbas  24296  eltsms  24301  tsmsres  24312  caussi  25467  causs  25468  elpwincl1  32882  disjdifprg2  32932  sigainb  34535  ldgenpisyslem1  34562  carsgclctun  34720  eulerpartlemgs2  34779  sseqval  34787  reprinrn  35014  bnj1177  35403  cvmsss2  35774  satef  35916  satefvfmla0  35918  fnemeet2  36906  ontgval  36970  bj-discrmoore  37781  bj-ideqb  37831  bj-opelidres  37833  bj-opelidb1ALT  37838  fin2so  38286  inex3  39015  inxpex  39016  dfrefrels2  39270  dfsymrels2  39302  dftrrels2  39336  elrfi  43453  ofoafg  44109  fourierdlem71  46919  fourierdlem80  46928  sge0less  47134  sge0ssre  47139  carageniuncllem2  47264  rngcbasALTV  49059  rngcrescrhmALTV  49073  ringcbasALTV  49093  srhmsubcALTV  49118  fldcALTV  49125  fldhmsubcALTV  49126