Theorem inex1g 5238

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 4136	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝐵) = (𝐴 ∩ 𝐵))
2	1	eleq1d 2823	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V))
3		vex 3426	. . 3 ⊢ 𝑥 ∈ V
4	3	inex1 5236	. 2 ⊢ (𝑥 ∩ 𝐵) ∈ V
5	2, 4	vtoclg 3495	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  Vcvv 3422   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890

This theorem is referenced by:  inex2g  5239  dmresexg  5904  predexg  6209  onin  6282  offval  7520  offval3  7798  frrlem13  8085  onsdominel  8862  ssenen  8887  inelfi  9107  fiin  9111  tskwe  9639  dfac8b  9718  ac10ct  9721  infpwfien  9749  fictb  9932  canthnum  10336  gruina  10505  ressinbas  16881  ressress  16884  qusin  17172  catcbas  17732  fpwipodrs  18173  psss  18213  gsumzres  19425  eltg  22015  eltg3  22020  ntrval  22095  restco  22223  restfpw  22238  ordtrest  22261  ordtrest2lem  22262  ordtrest2  22263  cnrmi  22419  restcnrm  22421  kgeni  22596  tsmsfbas  23187  eltsms  23192  tsmsres  23203  caussi  24366  causs  24367  elpwincl1  30775  disjdifprg2  30816  sigainb  32004  ldgenpisyslem1  32031  carsgclctun  32188  eulerpartlemgs2  32247  sseqval  32255  reprinrn  32498  bnj1177  32886  cvmsss2  33136  satef  33278  satefvfmla0  33280  fnemeet2  34483  ontgval  34547  bj-discrmoore  35209  bj-ideqb  35257  bj-opelidres  35259  bj-opelidb1ALT  35264  fin2so  35691  inex3  36400  inxpex  36401  dfrefrels2  36558  dfsymrels2  36586  dftrrels2  36616  elrfi  40432  iunrelexp0  41199  fourierdlem71  43608  fourierdlem80  43617  sge0less  43820  sge0ssre  43825  carageniuncllem2  43950  dfrngc2  45418  rnghmsscmap2  45419  rngcbasALTV  45429  dfringc2  45464  rhmsscmap2  45465  rhmsscrnghm  45472  rngcresringcat  45476  ringcbasALTV  45492  srhmsubc  45522  fldc  45529  fldhmsubc  45530  rngcrescrhm  45531  srhmsubcALTV  45540  fldcALTV  45547  fldhmsubcALTV  45548  rngcrescrhmALTV  45549