Theorem inex1g 5225

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 4183	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝐵) = (𝐴 ∩ 𝐵))
2	1	eleq1d 2899	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V))
3		vex 3499	. . 3 ⊢ 𝑥 ∈ V
4	3	inex1 5223	. 2 ⊢ (𝑥 ∩ 𝐵) ∈ V
5	2, 4	vtoclg 3569	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  Vcvv 3496   ∩ cin 3937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-in 3945

This theorem is referenced by:  inex2g  5226  dmresexg  5879  onin  6224  offval  7418  offval3  7685  onsdominel  8668  ssenen  8693  inelfi  8884  fiin  8888  tskwe  9381  dfac8b  9459  ac10ct  9462  infpwfien  9490  fictb  9669  canthnum  10073  gruina  10242  ressinbas  16562  ressress  16564  qusin  16819  catcbas  17359  fpwipodrs  17776  psss  17826  gsumzres  19031  eltg  21567  eltg3  21572  ntrval  21646  restco  21774  restfpw  21789  ordtrest  21812  ordtrest2lem  21813  ordtrest2  21814  cnrmi  21970  restcnrm  21972  kgeni  22147  tsmsfbas  22738  eltsms  22743  tsmsres  22754  caussi  23902  causs  23903  elpwincl1  30288  disjdifprg2  30328  sigainb  31397  ldgenpisyslem1  31424  carsgclctun  31581  eulerpartlemgs2  31640  sseqval  31648  reprinrn  31891  bnj1177  32280  cvmsss2  32523  satef  32665  satefvfmla0  32667  frrlem13  33137  fnemeet2  33717  ontgval  33781  bj-discrmoore  34405  bj-ideqb  34453  bj-opelidres  34455  bj-opelidb1ALT  34460  fin2so  34881  inex3  35597  inxpex  35598  dfrefrels2  35755  dfsymrels2  35783  dftrrels2  35813  elrfi  39298  iunrelexp0  40054  fourierdlem71  42469  fourierdlem80  42478  sge0less  42681  sge0ssre  42686  carageniuncllem2  42811  dfrngc2  44250  rnghmsscmap2  44251  rngcbasALTV  44261  dfringc2  44296  rhmsscmap2  44297  rhmsscrnghm  44304  rngcresringcat  44308  ringcbasALTV  44324  srhmsubc  44354  fldc  44361  fldhmsubc  44362  rngcrescrhm  44363  srhmsubcALTV  44372  fldcALTV  44379  fldhmsubcALTV  44380  rngcrescrhmALTV  44381