Theorem inex1g 5320

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 4206	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝐵) = (𝐴 ∩ 𝐵))
2	1	eleq1d 2819	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V))
3		vex 3479	. . 3 ⊢ 𝑥 ∈ V
4	3	inex1 5318	. 2 ⊢ (𝑥 ∩ 𝐵) ∈ V
5	2, 4	vtoclg 3557	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  Vcvv 3475   ∩ cin 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3956

This theorem is referenced by:  inex2g  5321  dmresexg  6006  predexg  6319  onin  6396  offval  7679  offval3  7969  frrlem13  8283  onsdominel  9126  ssenen  9151  inelfi  9413  fiin  9417  tskwe  9945  dfac8b  10026  ac10ct  10029  infpwfien  10057  fictb  10240  canthnum  10644  gruina  10813  ressinbas  17190  ressress  17193  qusin  17490  catcbas  18051  fpwipodrs  18493  psss  18533  gsumzres  19777  eltg  22460  eltg3  22465  ntrval  22540  restco  22668  restfpw  22683  ordtrest  22706  ordtrest2lem  22707  ordtrest2  22708  cnrmi  22864  restcnrm  22866  kgeni  23041  tsmsfbas  23632  eltsms  23637  tsmsres  23648  caussi  24814  causs  24815  elpwincl1  31794  disjdifprg2  31838  sigainb  33165  ldgenpisyslem1  33192  carsgclctun  33351  eulerpartlemgs2  33410  sseqval  33418  reprinrn  33661  bnj1177  34048  cvmsss2  34296  satef  34438  satefvfmla0  34440  fnemeet2  35300  ontgval  35364  bj-discrmoore  36040  bj-ideqb  36088  bj-opelidres  36090  bj-opelidb1ALT  36095  fin2so  36523  inex3  37255  inxpex  37256  dfrefrels2  37431  dfsymrels2  37463  dftrrels2  37493  elrfi  41480  ofoafg  42152  fourierdlem71  44941  fourierdlem80  44950  sge0less  45156  sge0ssre  45161  carageniuncllem2  45286  dfrngc2  46918  rnghmsscmap2  46919  rngcbasALTV  46929  dfringc2  46964  rhmsscmap2  46965  rhmsscrnghm  46972  rngcresringcat  46976  ringcbasALTV  46992  srhmsubc  47022  fldc  47029  fldhmsubc  47030  rngcrescrhm  47031  srhmsubcALTV  47040  fldcALTV  47047  fldhmsubcALTV  47048  rngcrescrhmALTV  47049