Theorem inex1g 5269

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3444   ∩ cin 3910

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 5246

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 3403  df-v 3446  df-in 3918

This theorem is referenced by:  inex2g  5270  dmresexg  5974  predexg  6280  onin  6351  offval  7642  offval3  7940  frrlem13  8254  onsdominel  9067  ssenen  9092  inelfi  9345  fiin  9349  tskwe  9879  dfac8b  9960  ac10ct  9963  infpwfien  9991  fictb  10173  canthnum  10578  gruina  10747  ressinbas  17191  ressress  17193  qusin  17483  catcbas  18043  fpwipodrs  18481  psss  18521  gsumzres  19823  dfrngc2  20548  rnghmsscmap2  20549  dfringc2  20577  rhmsscmap2  20578  rhmsscrnghm  20585  rngcresringcat  20589  srhmsubc  20600  rngcrescrhm  20604  fldc  20704  fldhmsubc  20705  eltg  22877  eltg3  22882  ntrval  22956  restco  23084  restfpw  23099  ordtrest  23122  ordtrest2lem  23123  ordtrest2  23124  cnrmi  23280  restcnrm  23282  kgeni  23457  tsmsfbas  24048  eltsms  24053  tsmsres  24064  caussi  25230  causs  25231  elpwincl1  32504  disjdifprg2  32555  sigainb  34119  ldgenpisyslem1  34146  carsgclctun  34305  eulerpartlemgs2  34364  sseqval  34372  reprinrn  34602  bnj1177  34989  cvmsss2  35254  satef  35396  satefvfmla0  35398  fnemeet2  36348  ontgval  36412  bj-discrmoore  37092  bj-ideqb  37140  bj-opelidres  37142  bj-opelidb1ALT  37147  fin2so  37594  inex3  38313  inxpex  38314  dfrefrels2  38497  dfsymrels2  38529  dftrrels2  38559  elrfi  42675  ofoafg  43336  fourierdlem71  46168  fourierdlem80  46177  sge0less  46383  sge0ssre  46388  carageniuncllem2  46513  rngcbasALTV  48247  rngcrescrhmALTV  48261  ringcbasALTV  48281  srhmsubcALTV  48306  fldcALTV  48313  fldhmsubcALTV  48314