Theorem inex1g 5314

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 4202	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝐵) = (𝐴 ∩ 𝐵))
2	1	eleq1d 2814	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V))
3		vex 3474	. . 3 ⊢ 𝑥 ∈ V
4	3	inex1 5312	. 2 ⊢ (𝑥 ∩ 𝐵) ∈ V
5	2, 4	vtoclg 3539	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099  Vcvv 3470   ∩ cin 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-sep 5294

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3429  df-v 3472  df-in 3952

This theorem is referenced by:  inex2g  5315  dmresexg  6004  predexg  6318  onin  6395  offval  7689  offval3  7981  frrlem13  8298  onsdominel  9145  ssenen  9170  inelfi  9436  fiin  9440  tskwe  9968  dfac8b  10049  ac10ct  10052  infpwfien  10080  fictb  10263  canthnum  10667  gruina  10836  ressinbas  17220  ressress  17223  qusin  17520  catcbas  18084  fpwipodrs  18526  psss  18566  gsumzres  19858  dfrngc2  20555  rnghmsscmap2  20556  dfringc2  20584  rhmsscmap2  20585  rhmsscrnghm  20592  rngcresringcat  20596  srhmsubc  20607  rngcrescrhm  20611  fldc  20666  fldhmsubc  20667  eltg  22854  eltg3  22859  ntrval  22934  restco  23062  restfpw  23077  ordtrest  23100  ordtrest2lem  23101  ordtrest2  23102  cnrmi  23258  restcnrm  23260  kgeni  23435  tsmsfbas  24026  eltsms  24031  tsmsres  24042  caussi  25219  causs  25220  elpwincl1  32316  disjdifprg2  32360  sigainb  33750  ldgenpisyslem1  33777  carsgclctun  33936  eulerpartlemgs2  33995  sseqval  34003  reprinrn  34245  bnj1177  34632  cvmsss2  34879  satef  35021  satefvfmla0  35023  fnemeet2  35846  ontgval  35910  bj-discrmoore  36585  bj-ideqb  36633  bj-opelidres  36635  bj-opelidb1ALT  36640  fin2so  37075  inex3  37805  inxpex  37806  dfrefrels2  37980  dfsymrels2  38012  dftrrels2  38042  elrfi  42105  ofoafg  42774  fourierdlem71  45556  fourierdlem80  45565  sge0less  45771  sge0ssre  45776  carageniuncllem2  45901  rngcbasALTV  47319  rngcrescrhmALTV  47333  ringcbasALTV  47353  srhmsubcALTV  47378  fldcALTV  47385  fldhmsubcALTV  47386