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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2146  Vcvv 3453   ∩ cin 4091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-sep 5251

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3416  df-v 3455  df-in 4093

This theorem is used by:  inex2g  5283  dmresexg  6010  predexg  6328  onin  6400  offval  7709  offval3  8001  frrlem13  8327  onsdominel  9156  ssenen  9181  inelfi  9420  fiin  9424  tskwe  10041  infpwfien  10151  fictb  10332  canthnum  10744  gruina  10913  ressinbas  17435  ressress  17437  qusin  17728  catcbas  18288  fpwipodrs  18726  acsmapd  18740  psss  18766  gsumzres  20135  dfrngc2  20892  rnghmsscmap2  20893  dfringc2  20921  rhmsscmap2  20922  rhmsscrnghm  20929  rngcresringcat  20933  srhmsubc  20944  rngcrescrhm  20948  fldc  21053  fldhmsubc  21054  eltg  23287  eltg3  23292  ntrval  23366  restco  23494  restfpw  23509  ordtrest  23532  ordtrest2lem  23533  ordtrest2  23534  cnrmi  23690  restcnrm  23692  kgeni  23868  tsmsfbas  24459  eltsms  24464  tsmsres  24475  caussi  25630  causs  25631  elpwincl1  33175  disjdifprg2  33224  sigainb  34822  ldgenpisyslem1  34849  carsgclctun  35006  eulerpartlemgs2  35065  sseqval  35073  reprinrn  35300  bnj1177  35689  cvmsss2  36160  satef  36302  satefvfmla0  36304  fnemeet2  37282  ontgval  37346  bj-discrmoore  38171  bj-ideqb  38220  bj-opelidres  38222  bj-opelidb1ALT  38227  fin2so  38670  inex3  39410  inxpex  39411  dfrefrels2  39665  dfsymrels2  39697  dftrrels2  39731  elrfi  43845  ofoafg  44496  fourierdlem71  47326  fourierdlem80  47335  sge0less  47541  sge0ssre  47546  carageniuncllem2  47671  rngcbasALTV  49502  rngcrescrhmALTV  49516  ringcbasALTV  49536  srhmsubcALTV  49561  fldcALTV  49568  fldhmsubcALTV  49569  parcoval  50901