Theorem inex1g 5244

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  Vcvv 3433   ∩ cin 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-sep 5224

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-in 3895

This theorem is referenced by:  inex2g  5245  dmresexg  5918  predexg  6224  onin  6301  offval  7551  offval3  7834  frrlem13  8123  onsdominel  8922  ssenen  8947  inelfi  9186  fiin  9190  tskwe  9717  dfac8b  9796  ac10ct  9799  infpwfien  9827  fictb  10010  canthnum  10414  gruina  10583  ressinbas  16964  ressress  16967  qusin  17264  catcbas  17825  fpwipodrs  18267  psss  18307  gsumzres  19519  eltg  22116  eltg3  22121  ntrval  22196  restco  22324  restfpw  22339  ordtrest  22362  ordtrest2lem  22363  ordtrest2  22364  cnrmi  22520  restcnrm  22522  kgeni  22697  tsmsfbas  23288  eltsms  23293  tsmsres  23304  caussi  24470  causs  24471  elpwincl1  30883  disjdifprg2  30924  sigainb  32113  ldgenpisyslem1  32140  carsgclctun  32297  eulerpartlemgs2  32356  sseqval  32364  reprinrn  32607  bnj1177  32995  cvmsss2  33245  satef  33387  satefvfmla0  33389  fnemeet2  34565  ontgval  34629  bj-discrmoore  35291  bj-ideqb  35339  bj-opelidres  35341  bj-opelidb1ALT  35346  fin2so  35773  inex3  36480  inxpex  36481  dfrefrels2  36638  dfsymrels2  36666  dftrrels2  36696  elrfi  40523  iunrelexp0  41317  fourierdlem71  43725  fourierdlem80  43734  sge0less  43937  sge0ssre  43942  carageniuncllem2  44067  dfrngc2  45541  rnghmsscmap2  45542  rngcbasALTV  45552  dfringc2  45587  rhmsscmap2  45588  rhmsscrnghm  45595  rngcresringcat  45599  ringcbasALTV  45615  srhmsubc  45645  fldc  45652  fldhmsubc  45653  rngcrescrhm  45654  srhmsubcALTV  45663  fldcALTV  45670  fldhmsubcALTV  45671  rngcrescrhmALTV  45672