Theorem inex1g 5319

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 4213	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝐵) = (𝐴 ∩ 𝐵))
2	1	eleq1d 2826	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V))
3		vex 3484	. . 3 ⊢ 𝑥 ∈ V
4	3	inex1 5317	. 2 ⊢ (𝑥 ∩ 𝐵) ∈ V
5	2, 4	vtoclg 3554	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  Vcvv 3480   ∩ cin 3950

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-in 3958

This theorem is referenced by:  inex2g  5320  dmresexg  6032  predexg  6339  onin  6415  offval  7706  offval3  8007  frrlem13  8323  onsdominel  9166  ssenen  9191  inelfi  9458  fiin  9462  tskwe  9990  dfac8b  10071  ac10ct  10074  infpwfien  10102  fictb  10284  canthnum  10689  gruina  10858  ressinbas  17291  ressress  17293  qusin  17589  catcbas  18146  fpwipodrs  18585  psss  18625  gsumzres  19927  dfrngc2  20628  rnghmsscmap2  20629  dfringc2  20657  rhmsscmap2  20658  rhmsscrnghm  20665  rngcresringcat  20669  srhmsubc  20680  rngcrescrhm  20684  fldc  20785  fldhmsubc  20786  eltg  22964  eltg3  22969  ntrval  23044  restco  23172  restfpw  23187  ordtrest  23210  ordtrest2lem  23211  ordtrest2  23212  cnrmi  23368  restcnrm  23370  kgeni  23545  tsmsfbas  24136  eltsms  24141  tsmsres  24152  caussi  25331  causs  25332  elpwincl1  32544  disjdifprg2  32589  sigainb  34137  ldgenpisyslem1  34164  carsgclctun  34323  eulerpartlemgs2  34382  sseqval  34390  reprinrn  34633  bnj1177  35020  cvmsss2  35279  satef  35421  satefvfmla0  35423  fnemeet2  36368  ontgval  36432  bj-discrmoore  37112  bj-ideqb  37160  bj-opelidres  37162  bj-opelidb1ALT  37167  fin2so  37614  inex3  38339  inxpex  38340  dfrefrels2  38514  dfsymrels2  38546  dftrrels2  38576  elrfi  42705  ofoafg  43367  fourierdlem71  46192  fourierdlem80  46201  sge0less  46407  sge0ssre  46412  carageniuncllem2  46537  rngcbasALTV  48182  rngcrescrhmALTV  48196  ringcbasALTV  48216  srhmsubcALTV  48241  fldcALTV  48248  fldhmsubcALTV  48249