Theorem inex1g 5246

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 4144	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝐵) = (𝐴 ∩ 𝐵))
2	1	eleq1d 2824	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V))
3		vex 3434	. . 3 ⊢ 𝑥 ∈ V
4	3	inex1 5244	. 2 ⊢ (𝑥 ∩ 𝐵) ∈ V
5	2, 4	vtoclg 3503	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2109  Vcvv 3430   ∩ cin 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710  ax-sep 5226

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3432  df-in 3898

This theorem is referenced by:  inex2g  5247  dmresexg  5912  predexg  6217  onin  6294  offval  7533  offval3  7811  frrlem13  8098  onsdominel  8878  ssenen  8903  inelfi  9138  fiin  9142  tskwe  9692  dfac8b  9771  ac10ct  9774  infpwfien  9802  fictb  9985  canthnum  10389  gruina  10558  ressinbas  16936  ressress  16939  qusin  17236  catcbas  17797  fpwipodrs  18239  psss  18279  gsumzres  19491  eltg  22088  eltg3  22093  ntrval  22168  restco  22296  restfpw  22311  ordtrest  22334  ordtrest2lem  22335  ordtrest2  22336  cnrmi  22492  restcnrm  22494  kgeni  22669  tsmsfbas  23260  eltsms  23265  tsmsres  23276  caussi  24442  causs  24443  elpwincl1  30853  disjdifprg2  30894  sigainb  32083  ldgenpisyslem1  32110  carsgclctun  32267  eulerpartlemgs2  32326  sseqval  32334  reprinrn  32577  bnj1177  32965  cvmsss2  33215  satef  33357  satefvfmla0  33359  fnemeet2  34535  ontgval  34599  bj-discrmoore  35261  bj-ideqb  35309  bj-opelidres  35311  bj-opelidb1ALT  35316  fin2so  35743  inex3  36452  inxpex  36453  dfrefrels2  36610  dfsymrels2  36638  dftrrels2  36668  elrfi  40496  iunrelexp0  41263  fourierdlem71  43672  fourierdlem80  43681  sge0less  43884  sge0ssre  43889  carageniuncllem2  44014  dfrngc2  45482  rnghmsscmap2  45483  rngcbasALTV  45493  dfringc2  45528  rhmsscmap2  45529  rhmsscrnghm  45536  rngcresringcat  45540  ringcbasALTV  45556  srhmsubc  45586  fldc  45593  fldhmsubc  45594  rngcrescrhm  45595  srhmsubcALTV  45604  fldcALTV  45611  fldhmsubcALTV  45612  rngcrescrhmALTV  45613