Theorem inex1g 5318

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 4204	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝐵) = (𝐴 ∩ 𝐵))
2	1	eleq1d 2818	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V))
3		vex 3478	. . 3 ⊢ 𝑥 ∈ V
4	3	inex1 5316	. 2 ⊢ (𝑥 ∩ 𝐵) ∈ V
5	2, 4	vtoclg 3556	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  Vcvv 3474   ∩ cin 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-in 3954

This theorem is referenced by:  inex2g  5319  dmresexg  6003  predexg  6315  onin  6392  offval  7675  offval3  7965  frrlem13  8279  onsdominel  9122  ssenen  9147  inelfi  9409  fiin  9413  tskwe  9941  dfac8b  10022  ac10ct  10025  infpwfien  10053  fictb  10236  canthnum  10640  gruina  10809  ressinbas  17186  ressress  17189  qusin  17486  catcbas  18047  fpwipodrs  18489  psss  18529  gsumzres  19771  eltg  22451  eltg3  22456  ntrval  22531  restco  22659  restfpw  22674  ordtrest  22697  ordtrest2lem  22698  ordtrest2  22699  cnrmi  22855  restcnrm  22857  kgeni  23032  tsmsfbas  23623  eltsms  23628  tsmsres  23639  caussi  24805  causs  24806  elpwincl1  31750  disjdifprg2  31794  sigainb  33122  ldgenpisyslem1  33149  carsgclctun  33308  eulerpartlemgs2  33367  sseqval  33375  reprinrn  33618  bnj1177  34005  cvmsss2  34253  satef  34395  satefvfmla0  34397  fnemeet2  35240  ontgval  35304  bj-discrmoore  35980  bj-ideqb  36028  bj-opelidres  36030  bj-opelidb1ALT  36035  fin2so  36463  inex3  37195  inxpex  37196  dfrefrels2  37371  dfsymrels2  37403  dftrrels2  37433  elrfi  41417  ofoafg  42089  fourierdlem71  44879  fourierdlem80  44888  sge0less  45094  sge0ssre  45099  carageniuncllem2  45224  dfrngc2  46823  rnghmsscmap2  46824  rngcbasALTV  46834  dfringc2  46869  rhmsscmap2  46870  rhmsscrnghm  46877  rngcresringcat  46881  ringcbasALTV  46897  srhmsubc  46927  fldc  46934  fldhmsubc  46935  rngcrescrhm  46936  srhmsubcALTV  46945  fldcALTV  46952  fldhmsubcALTV  46953  rngcrescrhmALTV  46954