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

Theorem inex1g 5215
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 4180 . . 3 (𝑥 = 𝐴 → (𝑥𝐵) = (𝐴𝐵))
21eleq1d 2897 . 2 (𝑥 = 𝐴 → ((𝑥𝐵) ∈ V ↔ (𝐴𝐵) ∈ V))
3 vex 3498 . . 3 𝑥 ∈ V
43inex1 5213 . 2 (𝑥𝐵) ∈ V
52, 4vtoclg 3568 1 (𝐴𝑉 → (𝐴𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105  Vcvv 3495  cin 3934
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-in 3942
This theorem is referenced by:  inex2g  5216  dmresexg  5871  onin  6216  offval  7405  offval3  7674  onsdominel  8655  ssenen  8680  inelfi  8871  fiin  8875  tskwe  9368  dfac8b  9446  ac10ct  9449  infpwfien  9477  fictb  9656  canthnum  10060  gruina  10229  ressinbas  16550  ressress  16552  qusin  16807  catcbas  17347  fpwipodrs  17764  psss  17814  gsumzres  18960  eltg  21495  eltg3  21500  ntrval  21574  restco  21702  restfpw  21717  ordtrest  21740  ordtrest2lem  21741  ordtrest2  21742  cnrmi  21898  restcnrm  21900  kgeni  22075  tsmsfbas  22665  eltsms  22670  tsmsres  22681  caussi  23829  causs  23830  elpwincl1  30214  disjdifprg2  30255  sigainb  31295  ldgenpisyslem1  31322  carsgclctun  31479  eulerpartlemgs2  31538  sseqval  31546  reprinrn  31789  bnj1177  32176  cvmsss2  32419  satef  32561  satefvfmla0  32563  frrlem13  33033  fnemeet2  33613  ontgval  33677  bj-discrmoore  34298  bj-ideqb  34344  bj-opelidres  34346  bj-opelidb1ALT  34351  fin2so  34761  inex3  35478  inxpex  35479  dfrefrels2  35635  dfsymrels2  35663  dftrrels2  35693  elrfi  39171  iunrelexp0  39927  fourierdlem71  42343  fourierdlem80  42352  sge0less  42555  sge0ssre  42560  carageniuncllem2  42685  dfrngc2  44141  rnghmsscmap2  44142  rngcbasALTV  44152  dfringc2  44187  rhmsscmap2  44188  rhmsscrnghm  44195  rngcresringcat  44199  ringcbasALTV  44215  srhmsubc  44245  fldc  44252  fldhmsubc  44253  rngcrescrhm  44254  srhmsubcALTV  44263  fldcALTV  44270  fldhmsubcALTV  44271  rngcrescrhmALTV  44272
  Copyright terms: Public domain W3C validator