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

Theorem inex1g 4173
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 3376 . . 3  |-  ( x  =  A  ->  (
x  i^i  B )  =  ( A  i^i  B ) )
21eleq1d 2362 . 2  |-  ( x  =  A  ->  (
( x  i^i  B
)  e.  _V  <->  ( A  i^i  B )  e.  _V ) )
3 vex 2804 . . 3  |-  x  e. 
_V
43inex1 4171 . 2  |-  ( x  i^i  B )  e. 
_V
52, 4vtoclg 2856 1  |-  ( A  e.  V  ->  ( A  i^i  B )  e. 
_V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    e. wcel 1696   _Vcvv 2801    i^i cin 3164
This theorem is referenced by:  onin  4439  dmresexg  4994  offval  6101  offval3  6107  onsdominel  7026  ssenen  7051  fiin  7191  tskwe  7599  dfac8b  7674  ac10ct  7677  infpwfien  7705  fictb  7887  canthnum  8287  gruina  8456  ressinbas  13220  ressress  13221  divsin  13462  catcbas  13945  fpwipodrs  14283  psss  14339  gsumzres  15210  eltg  16711  eltg3  16716  ntrval  16789  restco  16911  restfpw  16926  ordtrest  16948  ordtrest2lem  16949  ordtrest2  16950  cnrmi  17104  restcnrm  17106  kgeni  17248  tsmsfbas  17826  eltsms  17831  tsmsres  17842  caussi  18739  causs  18740  disjdifprg2  23368  sigainb  23512  cvmsss2  23820  epsetlike  24265  ontgval  24942  inpws1  25145  int2pre  25340  inposet  25381  islimrs4  25685  inttaror  26003  carinttar  26005  fnemeet2  26419  elrfi  26872  bnj1177  29352
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172
  Copyright terms: Public domain W3C validator