Theorem inex1g 5258

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3436   ∩ cin 3902

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 2701  ax-sep 5235

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-in 3910

This theorem is referenced by:  inex2g  5259  dmresexg  5965  predexg  6267  onin  6338  offval  7622  offval3  7917  frrlem13  8231  onsdominel  9043  ssenen  9068  inelfi  9308  fiin  9312  tskwe  9846  dfac8b  9925  ac10ct  9928  infpwfien  9956  fictb  10138  canthnum  10543  gruina  10712  ressinbas  17156  ressress  17158  qusin  17448  catcbas  18008  fpwipodrs  18446  psss  18486  gsumzres  19788  dfrngc2  20513  rnghmsscmap2  20514  dfringc2  20542  rhmsscmap2  20543  rhmsscrnghm  20550  rngcresringcat  20554  srhmsubc  20565  rngcrescrhm  20569  fldc  20669  fldhmsubc  20670  eltg  22842  eltg3  22847  ntrval  22921  restco  23049  restfpw  23064  ordtrest  23087  ordtrest2lem  23088  ordtrest2  23089  cnrmi  23245  restcnrm  23247  kgeni  23422  tsmsfbas  24013  eltsms  24018  tsmsres  24029  caussi  25195  causs  25196  elpwincl1  32469  disjdifprg2  32520  sigainb  34103  ldgenpisyslem1  34130  carsgclctun  34289  eulerpartlemgs2  34348  sseqval  34356  reprinrn  34586  bnj1177  34973  cvmsss2  35251  satef  35393  satefvfmla0  35395  fnemeet2  36345  ontgval  36409  bj-discrmoore  37089  bj-ideqb  37137  bj-opelidres  37139  bj-opelidb1ALT  37144  fin2so  37591  inex3  38310  inxpex  38311  dfrefrels2  38494  dfsymrels2  38526  dftrrels2  38556  elrfi  42671  ofoafg  43331  fourierdlem71  46162  fourierdlem80  46171  sge0less  46377  sge0ssre  46382  carageniuncllem2  46507  rngcbasALTV  48254  rngcrescrhmALTV  48268  ringcbasALTV  48288  srhmsubcALTV  48313  fldcALTV  48320  fldhmsubcALTV  48321