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

Theorem inex1g 4157
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 3363 . . 3  |-  ( x  =  A  ->  (
x  i^i  B )  =  ( A  i^i  B ) )
21eleq1d 2349 . 2  |-  ( x  =  A  ->  (
( x  i^i  B
)  e.  _V  <->  ( A  i^i  B )  e.  _V ) )
3 vex 2791 . . 3  |-  x  e. 
_V
43inex1 4155 . 2  |-  ( x  i^i  B )  e. 
_V
52, 4vtoclg 2843 1  |-  ( A  e.  V  ->  ( A  i^i  B )  e. 
_V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684   _Vcvv 2788    i^i cin 3151
This theorem is referenced by:  onin  4423  dmresexg  4978  offval  6085  offval3  6091  onsdominel  7010  ssenen  7035  fiin  7175  tskwe  7583  dfac8b  7658  ac10ct  7661  infpwfien  7689  fictb  7871  canthnum  8271  gruina  8440  ressinbas  13204  ressress  13205  divsin  13446  catcbas  13929  fpwipodrs  14267  psss  14323  gsumzres  15194  eltg  16695  eltg3  16700  ntrval  16773  restco  16895  restfpw  16910  ordtrest  16932  ordtrest2lem  16933  ordtrest2  16934  cnrmi  17088  restcnrm  17090  kgeni  17232  tsmsfbas  17810  eltsms  17815  tsmsres  17826  caussi  18723  causs  18724  disjdifprg2  23353  sigainb  23497  cvmsss2  23805  epsetlike  24194  ontgval  24870  inpws1  25042  int2pre  25237  inposet  25278  islimrs4  25582  inttaror  25900  carinttar  25902  fnemeet2  26316  elrfi  26769  bnj1177  29036
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159
  Copyright terms: Public domain W3C validator