Theorem inex1g 5337

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 4234	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝐵) = (𝐴 ∩ 𝐵))
2	1	eleq1d 2829	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V))
3		vex 3492	. . 3 ⊢ 𝑥 ∈ V
4	3	inex1 5335	. 2 ⊢ (𝑥 ∩ 𝐵) ∈ V
5	2, 4	vtoclg 3566	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  Vcvv 3488   ∩ cin 3975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-in 3983

This theorem is referenced by:  inex2g  5338  dmresexg  6043  predexg  6350  onin  6426  offval  7723  offval3  8023  frrlem13  8339  onsdominel  9192  ssenen  9217  inelfi  9487  fiin  9491  tskwe  10019  dfac8b  10100  ac10ct  10103  infpwfien  10131  fictb  10313  canthnum  10718  gruina  10887  ressinbas  17304  ressress  17307  qusin  17604  catcbas  18168  fpwipodrs  18610  psss  18650  gsumzres  19951  dfrngc2  20650  rnghmsscmap2  20651  dfringc2  20679  rhmsscmap2  20680  rhmsscrnghm  20687  rngcresringcat  20691  srhmsubc  20702  rngcrescrhm  20706  fldc  20807  fldhmsubc  20808  eltg  22985  eltg3  22990  ntrval  23065  restco  23193  restfpw  23208  ordtrest  23231  ordtrest2lem  23232  ordtrest2  23233  cnrmi  23389  restcnrm  23391  kgeni  23566  tsmsfbas  24157  eltsms  24162  tsmsres  24173  caussi  25350  causs  25351  elpwincl1  32555  disjdifprg2  32598  sigainb  34100  ldgenpisyslem1  34127  carsgclctun  34286  eulerpartlemgs2  34345  sseqval  34353  reprinrn  34595  bnj1177  34982  cvmsss2  35242  satef  35384  satefvfmla0  35386  fnemeet2  36333  ontgval  36397  bj-discrmoore  37077  bj-ideqb  37125  bj-opelidres  37127  bj-opelidb1ALT  37132  fin2so  37567  inex3  38294  inxpex  38295  dfrefrels2  38469  dfsymrels2  38501  dftrrels2  38531  elrfi  42650  ofoafg  43316  fourierdlem71  46098  fourierdlem80  46107  sge0less  46313  sge0ssre  46318  carageniuncllem2  46443  rngcbasALTV  47989  rngcrescrhmALTV  48003  ringcbasALTV  48023  srhmsubcALTV  48048  fldcALTV  48055  fldhmsubcALTV  48056