Theorem inex1g 5290

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 4174	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝐵) = (𝐴 ∩ 𝐵))
2	1	eleq1d 2854	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V))
3		vex 3467	. . 3 ⊢ 𝑥 ∈ V
4	3	inex1 5288	. 2 ⊢ (𝑥 ∩ 𝐵) ∈ V
5	2, 4	vtoclg 3531	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  Vcvv 3463   ∩ cin 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-in 3920

This theorem is referenced by:  inex2g  5291  dmresexg  6014  predexg  6321  onin  6393  offval  7684  offval3  7979  frrlem13  8295  onsdominel  9114  ssenen  9139  inelfi  9378  fiin  9382  tskwe  9936  dfac8b  10015  ac10ct  10018  infpwfien  10046  fictb  10227  canthnum  10634  gruina  10803  ressinbas  17305  ressress  17307  qusin  17598  catcbas  18158  fpwipodrs  18596  psss  18636  gsumzres  19979  dfrngc2  20713  rnghmsscmap2  20714  dfringc2  20742  rhmsscmap2  20743  rhmsscrnghm  20750  rngcresringcat  20754  srhmsubc  20765  rngcrescrhm  20769  fldc  20865  fldhmsubc  20866  eltg  23083  eltg3  23088  ntrval  23162  restco  23290  restfpw  23305  ordtrest  23328  ordtrest2lem  23329  ordtrest2  23330  cnrmi  23486  restcnrm  23488  kgeni  23663  tsmsfbas  24254  eltsms  24259  tsmsres  24270  caussi  25425  causs  25426  elpwincl1  32812  disjdifprg2  32862  sigainb  34471  ldgenpisyslem1  34498  carsgclctun  34656  eulerpartlemgs2  34715  sseqval  34723  reprinrn  34950  bnj1177  35339  cvmsss2  35699  satef  35841  satefvfmla0  35843  fnemeet2  36801  ontgval  36865  bj-discrmoore  37675  bj-ideqb  37725  bj-opelidres  37727  bj-opelidb1ALT  37732  fin2so  38180  inex3  38911  inxpex  38912  dfrefrels2  39166  dfsymrels2  39198  dftrrels2  39232  elrfi  43351  ofoafg  44007  fourierdlem71  46817  fourierdlem80  46826  sge0less  47032  sge0ssre  47037  carageniuncllem2  47162  rngcbasALTV  48954  rngcrescrhmALTV  48968  ringcbasALTV  48988  srhmsubcALTV  49013  fldcALTV  49020  fldhmsubcALTV  49021