Theorem inex1g 5294

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 4193	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝐵) = (𝐴 ∩ 𝐵))
2	1	eleq1d 2820	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V))
3		vex 3468	. . 3 ⊢ 𝑥 ∈ V
4	3	inex1 5292	. 2 ⊢ (𝑥 ∩ 𝐵) ∈ V
5	2, 4	vtoclg 3538	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3464   ∩ cin 3930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-sep 5271

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-in 3938

This theorem is referenced by:  inex2g  5295  dmresexg  6006  predexg  6313  onin  6388  offval  7685  offval3  7986  frrlem13  8302  onsdominel  9145  ssenen  9170  inelfi  9435  fiin  9439  tskwe  9969  dfac8b  10050  ac10ct  10053  infpwfien  10081  fictb  10263  canthnum  10668  gruina  10837  ressinbas  17271  ressress  17273  qusin  17563  catcbas  18119  fpwipodrs  18555  psss  18595  gsumzres  19895  dfrngc2  20593  rnghmsscmap2  20594  dfringc2  20622  rhmsscmap2  20623  rhmsscrnghm  20630  rngcresringcat  20634  srhmsubc  20645  rngcrescrhm  20649  fldc  20749  fldhmsubc  20750  eltg  22900  eltg3  22905  ntrval  22979  restco  23107  restfpw  23122  ordtrest  23145  ordtrest2lem  23146  ordtrest2  23147  cnrmi  23303  restcnrm  23305  kgeni  23480  tsmsfbas  24071  eltsms  24076  tsmsres  24087  caussi  25254  causs  25255  elpwincl1  32511  disjdifprg2  32562  sigainb  34172  ldgenpisyslem1  34199  carsgclctun  34358  eulerpartlemgs2  34417  sseqval  34425  reprinrn  34655  bnj1177  35042  cvmsss2  35301  satef  35443  satefvfmla0  35445  fnemeet2  36390  ontgval  36454  bj-discrmoore  37134  bj-ideqb  37182  bj-opelidres  37184  bj-opelidb1ALT  37189  fin2so  37636  inex3  38361  inxpex  38362  dfrefrels2  38536  dfsymrels2  38568  dftrrels2  38598  elrfi  42684  ofoafg  43345  fourierdlem71  46173  fourierdlem80  46182  sge0less  46388  sge0ssre  46393  carageniuncllem2  46518  rngcbasALTV  48208  rngcrescrhmALTV  48222  ringcbasALTV  48242  srhmsubcALTV  48267  fldcALTV  48274  fldhmsubcALTV  48275