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

Theorem inex1g 4349
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 3537 . . 3  |-  ( x  =  A  ->  (
x  i^i  B )  =  ( A  i^i  B ) )
21eleq1d 2504 . 2  |-  ( x  =  A  ->  (
( x  i^i  B
)  e.  _V  <->  ( A  i^i  B )  e.  _V ) )
3 vex 2961 . . 3  |-  x  e. 
_V
43inex1 4347 . 2  |-  ( x  i^i  B )  e. 
_V
52, 4vtoclg 3013 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 2958    i^i cin 3321
This theorem is referenced by:  onin  4615  dmresexg  5172  offval  6315  offval3  6321  onsdominel  7259  ssenen  7284  inelfi  7426  fiin  7430  tskwe  7842  dfac8b  7917  ac10ct  7920  infpwfien  7948  fictb  8130  canthnum  8529  gruina  8698  ressinbas  13530  ressress  13531  divsin  13774  catcbas  14257  fpwipodrs  14595  psss  14651  gsumzres  15522  eltg  17027  eltg3  17032  ntrval  17105  restco  17233  restfpw  17248  ordtrest  17271  ordtrest2lem  17272  ordtrest2  17273  cnrmi  17429  restcnrm  17431  kgeni  17574  tsmsfbas  18162  eltsms  18167  tsmsres  18178  caussi  19255  causs  19256  disjdifprg2  24023  sigainb  24524  cvmsss2  24966  epsetlike  25474  ontgval  26186  fnemeet2  26409  elrfi  26761  bnj1177  29448
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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 2419  ax-sep 4333
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 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-in 3329
  Copyright terms: Public domain W3C validator