Theorem inex1g 4595

Description: Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995.)

Assertion

Ref	Expression
inex1g

Proof of Theorem inex1g

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ineq1 3692	. . 3
2	1	eleq1d 2526	. 2
3		vex 3112	. . 3
4	3	inex1 4593	. 2
5	2, 4	vtoclg 3167	1

Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818  cvv 3109  i^icin 3474

This theorem is referenced by:  onin  4914  dmresexg  5301  offval  6547  offval3  6794  onsdominel  7686  ssenen  7711  inelfi  7898  fiin  7902  tskwe  8352  dfac8b  8433  ac10ct  8436  infpwfien  8464  fictb  8646  canthnum  9048  gruina  9217  ressinbas  14693  ressress  14694  qusin  14941  catcbas  15424  fpwipodrs  15794  psss  15844  gsumzres  16914  gsumzresOLD  16918  eltg  19458  eltg3  19463  ntrval  19537  restco  19665  restfpw  19680  ordtrest  19703  ordtrest2lem  19704  ordtrest2  19705  cnrmi  19861  restcnrm  19863  kgeni  20038  tsmsfbas  20626  eltsms  20631  tsmsresOLD  20645  tsmsres  20646  caussi  21736  causs  21737  disjdifprg2  27437  sigainb  28136  eulerpartlemgs2  28319  sseqval  28327  cvmsss2  28719  epsetlike  29274  ontgval  29896  fin2so  30040  fnemeet2  30185  elrfi  30626  fourierdlem71  31960  fourierdlem80  31969  dfrngc2  32780  rnghmsscmap2  32781  rngcbasOLD  32791  dfringc2  32826  rhmsscmap2  32827  rhmsscrnghm  32834  rngcresringcat  32838  ringcbasOLD  32854  srhmsubc  32884  fldc  32891  fldhmsubc  32892  rngcrescrhm  32893  srhmsubcOLD  32903  fldcOLD  32910  fldhmsubcOLD  32911  rngcrescrhmOLD  32912  bnj1177  34062  bj-diagval  34605

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482