Theorem inex1g 5260

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3429   ∩ cin 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-in 3896

This theorem is referenced by:  inex2g  5261  dmresexg  5979  predexg  6283  onin  6354  offval  7640  offval3  7935  frrlem13  8248  onsdominel  9064  ssenen  9089  inelfi  9331  fiin  9335  tskwe  9874  dfac8b  9953  ac10ct  9956  infpwfien  9984  fictb  10166  canthnum  10572  gruina  10741  ressinbas  17215  ressress  17217  qusin  17508  catcbas  18068  fpwipodrs  18506  psss  18546  gsumzres  19884  dfrngc2  20605  rnghmsscmap2  20606  dfringc2  20634  rhmsscmap2  20635  rhmsscrnghm  20642  rngcresringcat  20646  srhmsubc  20657  rngcrescrhm  20661  fldc  20761  fldhmsubc  20762  eltg  22922  eltg3  22927  ntrval  23001  restco  23129  restfpw  23144  ordtrest  23167  ordtrest2lem  23168  ordtrest2  23169  cnrmi  23325  restcnrm  23327  kgeni  23502  tsmsfbas  24093  eltsms  24098  tsmsres  24109  caussi  25264  causs  25265  elpwincl1  32595  disjdifprg2  32646  sigainb  34280  ldgenpisyslem1  34307  carsgclctun  34465  eulerpartlemgs2  34524  sseqval  34532  reprinrn  34762  bnj1177  35148  cvmsss2  35456  satef  35598  satefvfmla0  35600  fnemeet2  36549  ontgval  36613  bj-discrmoore  37423  bj-ideqb  37473  bj-opelidres  37475  bj-opelidb1ALT  37480  fin2so  37928  inex3  38659  inxpex  38660  dfrefrels2  38914  dfsymrels2  38946  dftrrels2  38980  elrfi  43126  ofoafg  43782  fourierdlem71  46605  fourierdlem80  46614  sge0less  46820  sge0ssre  46825  carageniuncllem2  46950  rngcbasALTV  48742  rngcrescrhmALTV  48756  ringcbasALTV  48776  srhmsubcALTV  48801  fldcALTV  48808  fldhmsubcALTV  48809