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

Theorem inex1g 5210
Description: Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995.)
Assertion
Ref Expression
inex1g (𝐴𝑉 → (𝐴𝐵) ∈ V)

Proof of Theorem inex1g
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 ineq1 4166 . . 3 (𝑥 = 𝐴 → (𝑥𝐵) = (𝐴𝐵))
21eleq1d 2900 . 2 (𝑥 = 𝐴 → ((𝑥𝐵) ∈ V ↔ (𝐴𝐵) ∈ V))
3 vex 3483 . . 3 𝑥 ∈ V
43inex1 5208 . 2 (𝑥𝐵) ∈ V
52, 4vtoclg 3553 1 (𝐴𝑉 → (𝐴𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2115  Vcvv 3480  cin 3918
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796  ax-sep 5190
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-rab 3142  df-v 3482  df-in 3926
This theorem is referenced by:  inex2g  5211  dmresexg  5866  onin  6211  offval  7412  offval3  7680  onsdominel  8665  ssenen  8690  inelfi  8881  fiin  8885  tskwe  9378  dfac8b  9457  ac10ct  9460  infpwfien  9488  fictb  9667  canthnum  10071  gruina  10240  ressinbas  16562  ressress  16564  qusin  16819  catcbas  17359  fpwipodrs  17776  psss  17826  gsumzres  19031  eltg  21571  eltg3  21576  ntrval  21650  restco  21778  restfpw  21793  ordtrest  21816  ordtrest2lem  21817  ordtrest2  21818  cnrmi  21974  restcnrm  21976  kgeni  22151  tsmsfbas  22742  eltsms  22747  tsmsres  22758  caussi  23910  causs  23911  elpwincl1  30304  disjdifprg2  30345  sigainb  31480  ldgenpisyslem1  31507  carsgclctun  31664  eulerpartlemgs2  31723  sseqval  31731  reprinrn  31974  bnj1177  32363  cvmsss2  32606  satef  32748  satefvfmla0  32750  frrlem13  33220  fnemeet2  33800  ontgval  33864  bj-discrmoore  34498  bj-ideqb  34546  bj-opelidres  34548  bj-opelidb1ALT  34553  fin2so  35016  inex3  35727  inxpex  35728  dfrefrels2  35885  dfsymrels2  35913  dftrrels2  35943  elrfi  39579  iunrelexp0  40347  fourierdlem71  42772  fourierdlem80  42781  sge0less  42984  sge0ssre  42989  carageniuncllem2  43114  dfrngc2  44549  rnghmsscmap2  44550  rngcbasALTV  44560  dfringc2  44595  rhmsscmap2  44596  rhmsscrnghm  44603  rngcresringcat  44607  ringcbasALTV  44623  srhmsubc  44653  fldc  44660  fldhmsubc  44661  rngcrescrhm  44662  srhmsubcALTV  44671  fldcALTV  44678  fldhmsubcALTV  44679  rngcrescrhmALTV  44680
  Copyright terms: Public domain W3C validator