Theorem inex1g 5320

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 4206	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝐵) = (𝐴 ∩ 𝐵))
2	1	eleq1d 2819	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V))
3		vex 3479	. . 3 ⊢ 𝑥 ∈ V
4	3	inex1 5318	. 2 ⊢ (𝑥 ∩ 𝐵) ∈ V
5	2, 4	vtoclg 3557	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  Vcvv 3475   ∩ cin 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3956

This theorem is referenced by:  inex2g  5321  dmresexg  6006  predexg  6319  onin  6396  offval  7679  offval3  7969  frrlem13  8283  onsdominel  9126  ssenen  9151  inelfi  9413  fiin  9417  tskwe  9945  dfac8b  10026  ac10ct  10029  infpwfien  10057  fictb  10240  canthnum  10644  gruina  10813  ressinbas  17190  ressress  17193  qusin  17490  catcbas  18051  fpwipodrs  18493  psss  18533  gsumzres  19777  eltg  22460  eltg3  22465  ntrval  22540  restco  22668  restfpw  22683  ordtrest  22706  ordtrest2lem  22707  ordtrest2  22708  cnrmi  22864  restcnrm  22866  kgeni  23041  tsmsfbas  23632  eltsms  23637  tsmsres  23648  caussi  24814  causs  24815  elpwincl1  31763  disjdifprg2  31807  sigainb  33134  ldgenpisyslem1  33161  carsgclctun  33320  eulerpartlemgs2  33379  sseqval  33387  reprinrn  33630  bnj1177  34017  cvmsss2  34265  satef  34407  satefvfmla0  34409  fnemeet2  35252  ontgval  35316  bj-discrmoore  35992  bj-ideqb  36040  bj-opelidres  36042  bj-opelidb1ALT  36047  fin2so  36475  inex3  37207  inxpex  37208  dfrefrels2  37383  dfsymrels2  37415  dftrrels2  37445  elrfi  41432  ofoafg  42104  fourierdlem71  44893  fourierdlem80  44902  sge0less  45108  sge0ssre  45113  carageniuncllem2  45238  dfrngc2  46870  rnghmsscmap2  46871  rngcbasALTV  46881  dfringc2  46916  rhmsscmap2  46917  rhmsscrnghm  46924  rngcresringcat  46928  ringcbasALTV  46944  srhmsubc  46974  fldc  46981  fldhmsubc  46982  rngcrescrhm  46983  srhmsubcALTV  46992  fldcALTV  46999  fldhmsubcALTV  47000  rngcrescrhmALTV  47001