Theorem inex1g 5275

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 4165	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝐵) = (𝐴 ∩ 𝐵))
2	1	eleq1d 2847	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V))
3		vex 3458	. . 3 ⊢ 𝑥 ∈ V
4	3	inex1 5273	. 2 ⊢ (𝑥 ∩ 𝐵) ∈ V
5	2, 4	vtoclg 3522	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142  Vcvv 3454   ∩ cin 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-in 3911

This theorem is referenced by:  inex2g  5276  dmresexg  6000  predexg  6306  onin  6377  offval  7669  offval3  7963  frrlem13  8279  onsdominel  9098  ssenen  9123  inelfi  9364  fiin  9368  tskwe  9908  dfac8b  9987  ac10ct  9990  infpwfien  10018  fictb  10200  canthnum  10607  gruina  10776  ressinbas  17281  ressress  17283  qusin  17574  catcbas  18134  fpwipodrs  18572  psss  18612  gsumzres  19949  dfrngc2  20678  rnghmsscmap2  20679  dfringc2  20707  rhmsscmap2  20708  rhmsscrnghm  20715  rngcresringcat  20719  srhmsubc  20730  rngcrescrhm  20734  fldc  20833  fldhmsubc  20834  eltg  23017  eltg3  23022  ntrval  23096  restco  23224  restfpw  23239  ordtrest  23262  ordtrest2lem  23263  ordtrest2  23264  cnrmi  23420  restcnrm  23422  kgeni  23597  tsmsfbas  24188  eltsms  24193  tsmsres  24204  caussi  25359  causs  25360  elpwincl1  32724  disjdifprg2  32776  sigainb  34433  ldgenpisyslem1  34460  carsgclctun  34618  eulerpartlemgs2  34677  sseqval  34685  reprinrn  34912  bnj1177  35301  cvmsss2  35624  satef  35766  satefvfmla0  35768  fnemeet2  36727  ontgval  36791  bj-discrmoore  37601  bj-ideqb  37651  bj-opelidres  37653  bj-opelidb1ALT  37658  fin2so  38106  inex3  38837  inxpex  38838  dfrefrels2  39092  dfsymrels2  39124  dftrrels2  39158  elrfi  43275  ofoafg  43931  fourierdlem71  46751  fourierdlem80  46760  sge0less  46966  sge0ssre  46971  carageniuncllem2  47096  rngcbasALTV  48888  rngcrescrhmALTV  48902  ringcbasALTV  48922  srhmsubcALTV  48947  fldcALTV  48954  fldhmsubcALTV  48955