Theorem inex1g 5262

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 4163	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝐵) = (𝐴 ∩ 𝐵))
2	1	eleq1d 2819	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V))
3		vex 3442	. . 3 ⊢ 𝑥 ∈ V
4	3	inex1 5260	. 2 ⊢ (𝑥 ∩ 𝐵) ∈ V
5	2, 4	vtoclg 3509	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  Vcvv 3438   ∩ cin 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-in 3906

This theorem is referenced by:  inex2g  5263  dmresexg  5971  predexg  6275  onin  6346  offval  7629  offval3  7924  frrlem13  8238  onsdominel  9052  ssenen  9077  inelfi  9319  fiin  9323  tskwe  9860  dfac8b  9939  ac10ct  9942  infpwfien  9970  fictb  10152  canthnum  10558  gruina  10727  ressinbas  17170  ressress  17172  qusin  17463  catcbas  18023  fpwipodrs  18461  psss  18501  gsumzres  19836  dfrngc2  20559  rnghmsscmap2  20560  dfringc2  20588  rhmsscmap2  20589  rhmsscrnghm  20596  rngcresringcat  20600  srhmsubc  20611  rngcrescrhm  20615  fldc  20715  fldhmsubc  20716  eltg  22899  eltg3  22904  ntrval  22978  restco  23106  restfpw  23121  ordtrest  23144  ordtrest2lem  23145  ordtrest2  23146  cnrmi  23302  restcnrm  23304  kgeni  23479  tsmsfbas  24070  eltsms  24075  tsmsres  24086  caussi  25251  causs  25252  elpwincl1  32549  disjdifprg2  32600  sigainb  34242  ldgenpisyslem1  34269  carsgclctun  34427  eulerpartlemgs2  34486  sseqval  34494  reprinrn  34724  bnj1177  35111  cvmsss2  35417  satef  35559  satefvfmla0  35561  fnemeet2  36510  ontgval  36574  bj-discrmoore  37255  bj-ideqb  37303  bj-opelidres  37305  bj-opelidb1ALT  37310  fin2so  37747  inex3  38470  inxpex  38471  dfrefrels2  38705  dfsymrels2  38737  dftrrels2  38771  elrfi  42878  ofoafg  43538  fourierdlem71  46363  fourierdlem80  46372  sge0less  46578  sge0ssre  46583  carageniuncllem2  46708  rngcbasALTV  48454  rngcrescrhmALTV  48468  ringcbasALTV  48488  srhmsubcALTV  48513  fldcALTV  48520  fldhmsubcALTV  48521