Theorem inex1g 5266

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 4167	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝐵) = (𝐴 ∩ 𝐵))
2	1	eleq1d 2822	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V))
3		vex 3446	. . 3 ⊢ 𝑥 ∈ V
4	3	inex1 5264	. 2 ⊢ (𝑥 ∩ 𝐵) ∈ V
5	2, 4	vtoclg 3513	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3442   ∩ cin 3902

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-in 3910

This theorem is referenced by:  inex2g  5267  dmresexg  5981  predexg  6285  onin  6356  offval  7641  offval3  7936  frrlem13  8250  onsdominel  9066  ssenen  9091  inelfi  9333  fiin  9337  tskwe  9874  dfac8b  9953  ac10ct  9956  infpwfien  9984  fictb  10166  canthnum  10572  gruina  10741  ressinbas  17184  ressress  17186  qusin  17477  catcbas  18037  fpwipodrs  18475  psss  18515  gsumzres  19850  dfrngc2  20573  rnghmsscmap2  20574  dfringc2  20602  rhmsscmap2  20603  rhmsscrnghm  20610  rngcresringcat  20614  srhmsubc  20625  rngcrescrhm  20629  fldc  20729  fldhmsubc  20730  eltg  22913  eltg3  22918  ntrval  22992  restco  23120  restfpw  23135  ordtrest  23158  ordtrest2lem  23159  ordtrest2  23160  cnrmi  23316  restcnrm  23318  kgeni  23493  tsmsfbas  24084  eltsms  24089  tsmsres  24100  caussi  25265  causs  25266  elpwincl1  32612  disjdifprg2  32663  sigainb  34314  ldgenpisyslem1  34341  carsgclctun  34499  eulerpartlemgs2  34558  sseqval  34566  reprinrn  34796  bnj1177  35182  cvmsss2  35490  satef  35632  satefvfmla0  35634  fnemeet2  36583  ontgval  36647  bj-discrmoore  37364  bj-ideqb  37414  bj-opelidres  37416  bj-opelidb1ALT  37421  fin2so  37858  inex3  38589  inxpex  38590  dfrefrels2  38844  dfsymrels2  38876  dftrrels2  38910  elrfi  43051  ofoafg  43711  fourierdlem71  46535  fourierdlem80  46544  sge0less  46750  sge0ssre  46755  carageniuncllem2  46880  rngcbasALTV  48626  rngcrescrhmALTV  48640  ringcbasALTV  48660  srhmsubcALTV  48685  fldcALTV  48692  fldhmsubcALTV  48693