Theorem inex1g 5076

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 4062	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝐵) = (𝐴 ∩ 𝐵))
2	1	eleq1d 2844	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V))
3		vex 3412	. . 3 ⊢ 𝑥 ∈ V
4	3	inex1 5074	. 2 ⊢ (𝑥 ∩ 𝐵) ∈ V
5	2, 4	vtoclg 3480	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

Syntax hints:   → wi 4   = wceq 1507   ∈ wcel 2050  Vcvv 3409   ∩ cin 3822

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2744  ax-sep 5056

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-rab 3091  df-v 3411  df-in 3830

This theorem is referenced by:  dmresexg  5719  onin  6057  offval  7232  offval3  7493  onsdominel  8460  ssenen  8485  inelfi  8675  fiin  8679  tskwe  9171  dfac8b  9249  ac10ct  9252  infpwfien  9280  fictb  9463  canthnum  9867  gruina  10036  ressinbas  16414  ressress  16416  qusin  16671  catcbas  17227  fpwipodrs  17644  psss  17694  gsumzres  18795  eltg  21281  eltg3  21286  ntrval  21360  restco  21488  restfpw  21503  ordtrest  21526  ordtrest2lem  21527  ordtrest2  21528  cnrmi  21684  restcnrm  21686  kgeni  21861  tsmsfbas  22451  eltsms  22456  tsmsres  22467  caussi  23615  causs  23616  elpwincl1  30072  disjdifprg2  30106  sigainb  31069  ldgenpisyslem1  31096  carsgclctun  31253  eulerpartlemgs2  31312  sseqval  31321  reprinrn  31566  bnj1177  31952  cvmsss2  32135  frrlem13  32685  fnemeet2  33265  ontgval  33328  bj-discrmoore  33943  bj-diagval  33973  fin2so  34349  inex2ALTV  35069  inex3  35070  inxpex  35071  dfrefrels2  35227  dfsymrels2  35255  dftrrels2  35285  elrfi  38715  iunrelexp0  39439  fourierdlem71  41918  fourierdlem80  41927  sge0less  42130  sge0ssre  42135  carageniuncllem2  42260  dfrngc2  43632  rnghmsscmap2  43633  rngcbasALTV  43643  dfringc2  43678  rhmsscmap2  43679  rhmsscrnghm  43686  rngcresringcat  43690  ringcbasALTV  43706  srhmsubc  43736  fldc  43743  fldhmsubc  43744  rngcrescrhm  43745  srhmsubcALTV  43754  fldcALTV  43761  fldhmsubcALTV  43762  rngcrescrhmALTV  43763  offval0  43957