Theorem inex1g 5279

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 4159	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝐵) = (𝐴 ∩ 𝐵))
2	1	eleq1d 2846	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V))
3		vex 3455	. . 3 ⊢ 𝑥 ∈ V
4	3	inex1 5277	. 2 ⊢ (𝑥 ∩ 𝐵) ∈ V
5	2, 4	vtoclg 3518	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  Vcvv 3451   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-in 3906

This theorem is used by:  inex2g  5280  dmresexg  6005  predexg  6322  onin  6394  offval  7702  offval3  7994  frrlem13  8316  onsdominel  9145  ssenen  9170  inelfi  9410  fiin  9414  tskwe  10031  infpwfien  10141  fictb  10322  canthnum  10734  gruina  10903  ressinbas  17423  ressress  17425  qusin  17716  catcbas  18276  fpwipodrs  18714  psss  18754  gsumzres  20123  dfrngc2  20880  rnghmsscmap2  20881  dfringc2  20909  rhmsscmap2  20910  rhmsscrnghm  20917  rngcresringcat  20921  srhmsubc  20932  rngcrescrhm  20936  fldc  21041  fldhmsubc  21042  eltg  23275  eltg3  23280  ntrval  23354  restco  23482  restfpw  23497  ordtrest  23520  ordtrest2lem  23521  ordtrest2  23522  cnrmi  23678  restcnrm  23680  kgeni  23856  tsmsfbas  24447  eltsms  24452  tsmsres  24463  caussi  25618  causs  25619  elpwincl1  33121  disjdifprg2  33170  sigainb  34769  ldgenpisyslem1  34796  carsgclctun  34953  eulerpartlemgs2  35012  sseqval  35020  reprinrn  35247  bnj1177  35636  cvmsss2  36039  satef  36181  satefvfmla0  36183  fnemeet2  37155  ontgval  37219  bj-discrmoore  38032  bj-ideqb  38080  bj-opelidres  38082  bj-opelidb1ALT  38087  fin2so  38530  inex3  39270  inxpex  39271  dfrefrels2  39525  dfsymrels2  39557  dftrrels2  39591  elrfi  43704  ofoafg  44355  fourierdlem71  47186  fourierdlem80  47195  sge0less  47401  sge0ssre  47406  carageniuncllem2  47531  rngcbasALTV  49362  rngcrescrhmALTV  49376  ringcbasALTV  49396  srhmsubcALTV  49421  fldcALTV  49428  fldhmsubcALTV  49429