Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  inex1g Structured version   Unicode version

Theorem inex1g 4347
 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.
StepHypRef Expression
1 ineq1 3536 . . 3
21eleq1d 2503 . 2
3 vex 2960 . . 3
43inex1 4345 . 2
52, 4vtoclg 3012 1
 Colors of variables: wff set class Syntax hints:   wi 4   wceq 1653   wcel 1726  cvv 2957   cin 3320 This theorem is referenced by:  onin  4613  dmresexg  5170  offval  6313  offval3  6319  onsdominel  7257  ssenen  7282  inelfi  7424  fiin  7428  tskwe  7838  dfac8b  7913  ac10ct  7916  infpwfien  7944  fictb  8126  canthnum  8525  gruina  8694  ressinbas  13526  ressress  13527  divsin  13770  catcbas  14253  fpwipodrs  14591  psss  14647  gsumzres  15518  eltg  17023  eltg3  17028  ntrval  17101  restco  17229  restfpw  17244  ordtrest  17267  ordtrest2lem  17268  ordtrest2  17269  cnrmi  17425  restcnrm  17427  kgeni  17570  tsmsfbas  18158  eltsms  18163  tsmsres  18174  caussi  19251  causs  19252  disjdifprg2  24019  sigainb  24520  cvmsss2  24962  epsetlike  25470  ontgval  26182  fnemeet2  26397  elrfi  26749  bnj1177  29376 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-sep 4331 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-v 2959  df-in 3328
 Copyright terms: Public domain W3C validator