Theorem inex1g 5255

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 4160	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝐵) = (𝐴 ∩ 𝐵))
2	1	eleq1d 2816	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V))
3		vex 3440	. . 3 ⊢ 𝑥 ∈ V
4	3	inex1 5253	. 2 ⊢ (𝑥 ∩ 𝐵) ∈ V
5	2, 4	vtoclg 3507	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  Vcvv 3436   ∩ cin 3896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-in 3904

This theorem is referenced by:  inex2g  5256  dmresexg  5962  predexg  6266  onin  6337  offval  7619  offval3  7914  frrlem13  8228  onsdominel  9039  ssenen  9064  inelfi  9302  fiin  9306  tskwe  9843  dfac8b  9922  ac10ct  9925  infpwfien  9953  fictb  10135  canthnum  10540  gruina  10709  ressinbas  17156  ressress  17158  qusin  17448  catcbas  18008  fpwipodrs  18446  psss  18486  gsumzres  19821  dfrngc2  20543  rnghmsscmap2  20544  dfringc2  20572  rhmsscmap2  20573  rhmsscrnghm  20580  rngcresringcat  20584  srhmsubc  20595  rngcrescrhm  20599  fldc  20699  fldhmsubc  20700  eltg  22872  eltg3  22877  ntrval  22951  restco  23079  restfpw  23094  ordtrest  23117  ordtrest2lem  23118  ordtrest2  23119  cnrmi  23275  restcnrm  23277  kgeni  23452  tsmsfbas  24043  eltsms  24048  tsmsres  24059  caussi  25224  causs  25225  elpwincl1  32505  disjdifprg2  32556  sigainb  34149  ldgenpisyslem1  34176  carsgclctun  34334  eulerpartlemgs2  34393  sseqval  34401  reprinrn  34631  bnj1177  35018  cvmsss2  35318  satef  35460  satefvfmla0  35462  fnemeet2  36411  ontgval  36475  bj-discrmoore  37155  bj-ideqb  37203  bj-opelidres  37205  bj-opelidb1ALT  37210  fin2so  37657  inex3  38380  inxpex  38381  dfrefrels2  38615  dfsymrels2  38647  dftrrels2  38681  elrfi  42797  ofoafg  43457  fourierdlem71  46285  fourierdlem80  46294  sge0less  46500  sge0ssre  46505  carageniuncllem2  46630  rngcbasALTV  48376  rngcrescrhmALTV  48390  ringcbasALTV  48410  srhmsubcALTV  48435  fldcALTV  48442  fldhmsubcALTV  48443