Theorem inex1g 5290

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 4166	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝐵) = (𝐴 ∩ 𝐵))
2	1	eleq1d 2850	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V))
3		vex 3461	. . 3 ⊢ 𝑥 ∈ V
4	3	inex1 5288	. 2 ⊢ (𝑥 ∩ 𝐵) ∈ V
5	2, 4	vtoclg 3524	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  Vcvv 3457   ∩ cin 3905

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-in 3913

This theorem is used by:  inex2g  5291  dmresexg  6015  predexg  6324  onin  6396  offval  7693  offval3  7985  frrlem13  8301  onsdominel  9121  ssenen  9146  inelfi  9385  fiin  9389  tskwe  9952  infpwfien  10062  fictb  10243  canthnum  10651  gruina  10820  ressinbas  17329  ressress  17331  qusin  17622  catcbas  18182  fpwipodrs  18620  psss  18660  gsumzres  20025  dfrngc2  20779  rnghmsscmap2  20780  dfringc2  20808  rhmsscmap2  20809  rhmsscrnghm  20816  rngcresringcat  20820  srhmsubc  20831  rngcrescrhm  20835  fldc  20939  fldhmsubc  20940  eltg  23166  eltg3  23171  ntrval  23245  restco  23373  restfpw  23388  ordtrest  23411  ordtrest2lem  23412  ordtrest2  23413  cnrmi  23569  restcnrm  23571  kgeni  23747  tsmsfbas  24338  eltsms  24343  tsmsres  24354  caussi  25509  causs  25510  elpwincl1  32944  disjdifprg2  32994  sigainb  34593  ldgenpisyslem1  34620  carsgclctun  34778  eulerpartlemgs2  34837  sseqval  34845  reprinrn  35072  bnj1177  35461  cvmsss2  35805  satef  35947  satefvfmla0  35949  fnemeet2  36937  ontgval  37001  bj-discrmoore  37812  bj-ideqb  37862  bj-opelidres  37864  bj-opelidb1ALT  37869  fin2so  38317  inex3  39047  inxpex  39048  dfrefrels2  39302  dfsymrels2  39334  dftrrels2  39368  elrfi  43485  ofoafg  44141  fourierdlem71  46951  fourierdlem80  46960  sge0less  47166  sge0ssre  47171  carageniuncllem2  47296  rngcbasALTV  49090  rngcrescrhmALTV  49104  ringcbasALTV  49124  srhmsubcALTV  49149  fldcALTV  49156  fldhmsubcALTV  49157