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

Theorem inex1g 4546
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 3656 . . 3  |-  ( x  =  A  ->  (
x  i^i  B )  =  ( A  i^i  B ) )
21eleq1d 2523 . 2  |-  ( x  =  A  ->  (
( x  i^i  B
)  e.  _V  <->  ( A  i^i  B )  e.  _V ) )
3 vex 3081 . . 3  |-  x  e. 
_V
43inex1 4544 . 2  |-  ( x  i^i  B )  e. 
_V
52, 4vtoclg 3136 1  |-  ( A  e.  V  ->  ( A  i^i  B )  e. 
_V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    e. wcel 1758   _Vcvv 3078    i^i cin 3438
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4524
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-in 3446
This theorem is referenced by:  onin  4861  dmresexg  5244  offval  6440  offval3  6684  onsdominel  7573  ssenen  7598  inelfi  7782  fiin  7786  tskwe  8234  dfac8b  8315  ac10ct  8318  infpwfien  8346  fictb  8528  canthnum  8930  gruina  9099  ressinbas  14356  ressress  14357  divsin  14604  catcbas  15087  fpwipodrs  15456  psss  15506  gsumzres  16512  gsumzresOLD  16516  eltg  18697  eltg3  18702  ntrval  18775  restco  18903  restfpw  18918  ordtrest  18941  ordtrest2lem  18942  ordtrest2  18943  cnrmi  19099  restcnrm  19101  kgeni  19245  tsmsfbas  19833  eltsms  19838  tsmsresOLD  19852  tsmsres  19853  caussi  20943  causs  20944  disjdifprg2  26091  sigainb  26744  eulerpartlemgs2  26927  sseqval  26935  cvmsss2  27327  epsetlike  27819  ontgval  28441  fin2so  28584  fnemeet2  28756  elrfi  29198  bnj1177  32349  bj-diagval  32883
  Copyright terms: Public domain W3C validator