Theorem inex1g 5282

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 4159	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝐵) = (𝐴 ∩ 𝐵))
2	1	eleq1d 2845	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V))
3		vex 3454	. . 3 ⊢ 𝑥 ∈ V
4	3	inex1 5280	. 2 ⊢ (𝑥 ∩ 𝐵) ∈ V
5	2, 4	vtoclg 3517	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  Vcvv 3450   ∩ cin 3898

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 2147  ax-9 2155  ax-ext 2732  ax-sep 5251

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-in 3906

This theorem is used by:  inex2g  5283  dmresexg  6007  predexg  6317  onin  6389  offval  7688  offval3  7980  frrlem13  8298  onsdominel  9127  ssenen  9152  inelfi  9391  fiin  9395  tskwe  9958  infpwfien  10068  fictb  10249  canthnum  10661  gruina  10830  ressinbas  17340  ressress  17342  qusin  17633  catcbas  18193  fpwipodrs  18631  psss  18671  gsumzres  20039  dfrngc2  20793  rnghmsscmap2  20794  dfringc2  20822  rhmsscmap2  20823  rhmsscrnghm  20830  rngcresringcat  20834  srhmsubc  20845  rngcrescrhm  20849  fldc  20953  fldhmsubc  20954  eltg  23185  eltg3  23190  ntrval  23264  restco  23392  restfpw  23407  ordtrest  23430  ordtrest2lem  23431  ordtrest2  23432  cnrmi  23588  restcnrm  23590  kgeni  23766  tsmsfbas  24357  eltsms  24362  tsmsres  24373  caussi  25528  causs  25529  elpwincl1  33003  disjdifprg2  33052  sigainb  34650  ldgenpisyslem1  34677  carsgclctun  34835  eulerpartlemgs2  34894  sseqval  34902  reprinrn  35129  bnj1177  35518  cvmsss2  35856  satef  35998  satefvfmla0  36000  fnemeet2  36989  ontgval  37053  bj-discrmoore  37864  bj-ideqb  37914  bj-opelidres  37916  bj-opelidb1ALT  37921  fin2so  38364  inex3  39089  inxpex  39090  dfrefrels2  39344  dfsymrels2  39376  dftrrels2  39410  elrfi  43542  ofoafg  44198  fourierdlem71  47008  fourierdlem80  47017  sge0less  47223  sge0ssre  47228  carageniuncllem2  47353  rngcbasALTV  49184  rngcrescrhmALTV  49198  ringcbasALTV  49218  srhmsubcALTV  49243  fldcALTV  49250  fldhmsubcALTV  49251