Theorem inex1g 5274

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 4176	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝐵) = (𝐴 ∩ 𝐵))
2	1	eleq1d 2813	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V))
3		vex 3451	. . 3 ⊢ 𝑥 ∈ V
4	3	inex1 5272	. 2 ⊢ (𝑥 ∩ 𝐵) ∈ V
5	2, 4	vtoclg 3520	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3447   ∩ cin 3913

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-in 3921

This theorem is referenced by:  inex2g  5275  dmresexg  5985  predexg  6292  onin  6363  offval  7662  offval3  7961  frrlem13  8277  onsdominel  9090  ssenen  9115  inelfi  9369  fiin  9373  tskwe  9903  dfac8b  9984  ac10ct  9987  infpwfien  10015  fictb  10197  canthnum  10602  gruina  10771  ressinbas  17215  ressress  17217  qusin  17507  catcbas  18063  fpwipodrs  18499  psss  18539  gsumzres  19839  dfrngc2  20537  rnghmsscmap2  20538  dfringc2  20566  rhmsscmap2  20567  rhmsscrnghm  20574  rngcresringcat  20578  srhmsubc  20589  rngcrescrhm  20593  fldc  20693  fldhmsubc  20694  eltg  22844  eltg3  22849  ntrval  22923  restco  23051  restfpw  23066  ordtrest  23089  ordtrest2lem  23090  ordtrest2  23091  cnrmi  23247  restcnrm  23249  kgeni  23424  tsmsfbas  24015  eltsms  24020  tsmsres  24031  caussi  25197  causs  25198  elpwincl1  32454  disjdifprg2  32505  sigainb  34126  ldgenpisyslem1  34153  carsgclctun  34312  eulerpartlemgs2  34371  sseqval  34379  reprinrn  34609  bnj1177  34996  cvmsss2  35261  satef  35403  satefvfmla0  35405  fnemeet2  36355  ontgval  36419  bj-discrmoore  37099  bj-ideqb  37147  bj-opelidres  37149  bj-opelidb1ALT  37154  fin2so  37601  inex3  38320  inxpex  38321  dfrefrels2  38504  dfsymrels2  38536  dftrrels2  38566  elrfi  42682  ofoafg  43343  fourierdlem71  46175  fourierdlem80  46184  sge0less  46390  sge0ssre  46395  carageniuncllem2  46520  rngcbasALTV  48251  rngcrescrhmALTV  48265  ringcbasALTV  48285  srhmsubcALTV  48310  fldcALTV  48317  fldhmsubcALTV  48318