Theorem inex1g 5264

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 2821	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V))
3		vex 3444	. . 3 ⊢ 𝑥 ∈ V
4	3	inex1 5262	. 2 ⊢ (𝑥 ∩ 𝐵) ∈ V
5	2, 4	vtoclg 3511	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  Vcvv 3440   ∩ cin 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-in 3908

This theorem is referenced by:  inex2g  5265  dmresexg  5973  predexg  6277  onin  6348  offval  7631  offval3  7926  frrlem13  8240  onsdominel  9054  ssenen  9079  inelfi  9321  fiin  9325  tskwe  9862  dfac8b  9941  ac10ct  9944  infpwfien  9972  fictb  10154  canthnum  10560  gruina  10729  ressinbas  17172  ressress  17174  qusin  17465  catcbas  18025  fpwipodrs  18463  psss  18503  gsumzres  19838  dfrngc2  20561  rnghmsscmap2  20562  dfringc2  20590  rhmsscmap2  20591  rhmsscrnghm  20598  rngcresringcat  20602  srhmsubc  20613  rngcrescrhm  20617  fldc  20717  fldhmsubc  20718  eltg  22901  eltg3  22906  ntrval  22980  restco  23108  restfpw  23123  ordtrest  23146  ordtrest2lem  23147  ordtrest2  23148  cnrmi  23304  restcnrm  23306  kgeni  23481  tsmsfbas  24072  eltsms  24077  tsmsres  24088  caussi  25253  causs  25254  elpwincl1  32600  disjdifprg2  32651  sigainb  34293  ldgenpisyslem1  34320  carsgclctun  34478  eulerpartlemgs2  34537  sseqval  34545  reprinrn  34775  bnj1177  35162  cvmsss2  35468  satef  35610  satefvfmla0  35612  fnemeet2  36561  ontgval  36625  bj-discrmoore  37316  bj-ideqb  37364  bj-opelidres  37366  bj-opelidb1ALT  37371  fin2so  37808  inex3  38533  inxpex  38534  dfrefrels2  38776  dfsymrels2  38808  dftrrels2  38842  elrfi  42946  ofoafg  43606  fourierdlem71  46431  fourierdlem80  46440  sge0less  46646  sge0ssre  46651  carageniuncllem2  46776  rngcbasALTV  48522  rngcrescrhmALTV  48536  ringcbasALTV  48556  srhmsubcALTV  48581  fldcALTV  48588  fldhmsubcALTV  48589