Theorem inex1g 5257

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3430   ∩ cin 3889

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 5232

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 3391  df-v 3432  df-in 3897

This theorem is referenced by:  inex2g  5258  dmresexg  5974  predexg  6278  onin  6349  offval  7634  offval3  7929  frrlem13  8242  onsdominel  9058  ssenen  9083  inelfi  9325  fiin  9329  tskwe  9868  dfac8b  9947  ac10ct  9950  infpwfien  9978  fictb  10160  canthnum  10566  gruina  10735  ressinbas  17209  ressress  17211  qusin  17502  catcbas  18062  fpwipodrs  18500  psss  18540  gsumzres  19878  dfrngc2  20599  rnghmsscmap2  20600  dfringc2  20628  rhmsscmap2  20629  rhmsscrnghm  20636  rngcresringcat  20640  srhmsubc  20651  rngcrescrhm  20655  fldc  20755  fldhmsubc  20756  eltg  22935  eltg3  22940  ntrval  23014  restco  23142  restfpw  23157  ordtrest  23180  ordtrest2lem  23181  ordtrest2  23182  cnrmi  23338  restcnrm  23340  kgeni  23515  tsmsfbas  24106  eltsms  24111  tsmsres  24122  caussi  25277  causs  25278  elpwincl1  32613  disjdifprg2  32664  sigainb  34299  ldgenpisyslem1  34326  carsgclctun  34484  eulerpartlemgs2  34543  sseqval  34551  reprinrn  34781  bnj1177  35167  cvmsss2  35475  satef  35617  satefvfmla0  35619  fnemeet2  36568  ontgval  36632  bj-discrmoore  37442  bj-ideqb  37492  bj-opelidres  37494  bj-opelidb1ALT  37499  fin2so  37945  inex3  38676  inxpex  38677  dfrefrels2  38931  dfsymrels2  38963  dftrrels2  38997  elrfi  43143  ofoafg  43803  fourierdlem71  46626  fourierdlem80  46635  sge0less  46841  sge0ssre  46846  carageniuncllem2  46971  rngcbasALTV  48757  rngcrescrhmALTV  48771  ringcbasALTV  48791  srhmsubcALTV  48816  fldcALTV  48823  fldhmsubcALTV  48824