Theorem inex1g 4935

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 3958	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝐵) = (𝐴 ∩ 𝐵))
2	1	eleq1d 2835	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V))
3		vex 3354	. . 3 ⊢ 𝑥 ∈ V
4	3	inex1 4933	. 2 ⊢ (𝑥 ∩ 𝐵) ∈ V
5	2, 4	vtoclg 3417	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

Syntax hints:   → wi 4   = wceq 1631   ∈ wcel 2145  Vcvv 3351   ∩ cin 3722

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-in 3730

This theorem is referenced by:  dmresexg  5562  onin  5897  offval  7051  offval3  7309  onsdominel  8265  ssenen  8290  inelfi  8480  fiin  8484  tskwe  8976  dfac8b  9054  ac10ct  9057  infpwfien  9085  fictb  9269  canthnum  9673  gruina  9842  ressinbas  16143  ressress  16146  qusin  16412  catcbas  16954  fpwipodrs  17372  psss  17422  gsumzres  18517  eltg  20982  eltg3  20987  ntrval  21061  restco  21189  restfpw  21204  ordtrest  21227  ordtrest2lem  21228  ordtrest2  21229  cnrmi  21385  restcnrm  21387  kgeni  21561  tsmsfbas  22151  eltsms  22156  tsmsres  22167  caussi  23314  causs  23315  elpwincl1  29695  disjdifprg2  29727  sigainb  30539  ldgenpisyslem1  30566  carsgclctun  30723  eulerpartlemgs2  30782  sseqval  30790  reprinrn  31036  bnj1177  31412  cvmsss2  31594  fnemeet2  32699  ontgval  32767  bj-discrmoore  33398  bj-diagval  33427  fin2so  33729  inex2ALTV  34448  inex3  34449  inxpex  34450  dfrefrels2  34605  dfsymrels2  34633  elrfi  37783  iunrelexp0  38520  fourierdlem71  40911  fourierdlem80  40920  sge0less  41126  sge0ssre  41131  carageniuncllem2  41256  dfrngc2  42500  rnghmsscmap2  42501  rngcbasALTV  42511  dfringc2  42546  rhmsscmap2  42547  rhmsscrnghm  42554  rngcresringcat  42558  ringcbasALTV  42574  srhmsubc  42604  fldc  42611  fldhmsubc  42612  rngcrescrhm  42613  srhmsubcALTV  42622  fldcALTV  42629  fldhmsubcALTV  42630  rngcrescrhmALTV  42631  offval0  42827