Theorem inex1g 4729

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 3769	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝐵) = (𝐴 ∩ 𝐵))
2	1	eleq1d 2672	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V))
3		vex 3176	. . 3 ⊢ 𝑥 ∈ V
4	3	inex1 4727	. 2 ⊢ (𝑥 ∩ 𝐵) ∈ V
5	2, 4	vtoclg 3239	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977  Vcvv 3173   ∩ cin 3539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547

This theorem is referenced by:  dmresexg  5341  onin  5671  offval  6802  offval3  7053  onsdominel  7994  ssenen  8019  inelfi  8207  fiin  8211  tskwe  8659  dfac8b  8737  ac10ct  8740  infpwfien  8768  fictb  8950  canthnum  9350  gruina  9519  ressinbas  15763  ressress  15765  qusin  16027  catcbas  16570  fpwipodrs  16987  psss  17037  gsumzres  18133  eltg  20572  eltg3  20577  ntrval  20650  restco  20778  restfpw  20793  ordtrest  20816  ordtrest2lem  20817  ordtrest2  20818  cnrmi  20974  restcnrm  20976  kgeni  21150  tsmsfbas  21741  eltsms  21746  tsmsres  21757  caussi  22903  causs  22904  elpwincl1  28741  disjdifprg2  28771  sigainb  29526  ldgenpisyslem1  29553  carsgclctun  29710  eulerpartlemgs2  29769  sseqval  29777  bnj1177  30328  cvmsss2  30510  fnemeet2  31532  ontgval  31600  bj-diagval  32267  fin2so  32566  elrfi  36275  iunrelexp0  37013  fourierdlem71  39070  fourierdlem80  39079  sge0less  39285  sge0ssre  39290  carageniuncllem2  39412  dfrngc2  41764  rnghmsscmap2  41765  rngcbasALTV  41775  dfringc2  41810  rhmsscmap2  41811  rhmsscrnghm  41818  rngcresringcat  41822  ringcbasALTV  41838  srhmsubc  41868  fldc  41875  fldhmsubc  41876  rngcrescrhm  41877  srhmsubcALTV  41887  fldcALTV  41894  fldhmsubcALTV  41895  rngcrescrhmALTV  41896  offval0  42093