Theorem inex1g 5247

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  Vcvv 3431   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-in 3890

This theorem is referenced by:  inex2g  5248  dmresexg  5966  predexg  6270  onin  6341  offval  7629  offval3  7924  frrlem13  8238  onsdominel  9054  ssenen  9079  inelfi  9321  fiin  9325  tskwe  9865  dfac8b  9944  ac10ct  9947  infpwfien  9975  fictb  10157  canthnum  10563  gruina  10732  ressinbas  17206  ressress  17208  qusin  17499  catcbas  18059  fpwipodrs  18497  psss  18537  gsumzres  19875  dfrngc2  20600  rnghmsscmap2  20601  dfringc2  20629  rhmsscmap2  20630  rhmsscrnghm  20637  rngcresringcat  20641  srhmsubc  20652  rngcrescrhm  20656  fldc  20756  fldhmsubc  20757  eltg  22940  eltg3  22945  ntrval  23019  restco  23147  restfpw  23162  ordtrest  23185  ordtrest2lem  23186  ordtrest2  23187  cnrmi  23343  restcnrm  23345  kgeni  23520  tsmsfbas  24111  eltsms  24116  tsmsres  24127  caussi  25282  causs  25283  elpwincl1  32613  disjdifprg2  32665  sigainb  34320  ldgenpisyslem1  34347  carsgclctun  34505  eulerpartlemgs2  34564  sseqval  34572  reprinrn  34802  bnj1177  35188  cvmsss2  35502  satef  35644  satefvfmla0  35646  fnemeet2  36595  ontgval  36659  bj-discrmoore  37469  bj-ideqb  37519  bj-opelidres  37521  bj-opelidb1ALT  37526  fin2so  37974  inex3  38705  inxpex  38706  dfrefrels2  38960  dfsymrels2  38992  dftrrels2  39026  elrfi  43143  ofoafg  43799  fourierdlem71  46620  fourierdlem80  46629  sge0less  46835  sge0ssre  46840  carageniuncllem2  46965  rngcbasALTV  48757  rngcrescrhmALTV  48771  ringcbasALTV  48791  srhmsubcALTV  48816  fldcALTV  48823  fldhmsubcALTV  48824