MPE Home 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  |-  ( A  e.  V  ->  ( A  i^i  B )  e. 
_V )

Proof of Theorem inex1g
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 ineq1 3536 . . 3  |-  ( x  =  A  ->  (
x  i^i  B )  =  ( A  i^i  B ) )
21eleq1d 2503 . 2  |-  ( x  =  A  ->  (
( x  i^i  B
)  e.  _V  <->  ( A  i^i  B )  e.  _V ) )
3 vex 2960 . . 3  |-  x  e. 
_V
43inex1 4345 . 2  |-  ( x  i^i  B )  e. 
_V
52, 4vtoclg 3012 1  |-  ( A  e.  V  ->  ( A  i^i  B )  e. 
_V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    e. wcel 1726   _Vcvv 2957    i^i 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