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

Theorem inex1 4052
Description: Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
inex1.1  |-  A  e. 
_V
Assertion
Ref Expression
inex1  |-  ( A  i^i  B )  e. 
_V

Proof of Theorem inex1
StepHypRef Expression
1 inex1.1 . . . 4  |-  A  e. 
_V
21zfauscl 4040 . . 3  |-  E. x A. y ( y  e.  x  <->  ( y  e.  A  /\  y  e.  B ) )
3 dfcleq 2247 . . . . 5  |-  ( x  =  ( A  i^i  B )  <->  A. y ( y  e.  x  <->  y  e.  ( A  i^i  B ) ) )
4 elin 3266 . . . . . . 7  |-  ( y  e.  ( A  i^i  B )  <->  ( y  e.  A  /\  y  e.  B ) )
54bibi2i 306 . . . . . 6  |-  ( ( y  e.  x  <->  y  e.  ( A  i^i  B ) )  <->  ( y  e.  x  <->  ( y  e.  A  /\  y  e.  B ) ) )
65albii 1554 . . . . 5  |-  ( A. y ( y  e.  x  <->  y  e.  ( A  i^i  B ) )  <->  A. y ( y  e.  x  <->  ( y  e.  A  /\  y  e.  B ) ) )
73, 6bitri 242 . . . 4  |-  ( x  =  ( A  i^i  B )  <->  A. y ( y  e.  x  <->  ( y  e.  A  /\  y  e.  B ) ) )
87exbii 1580 . . 3  |-  ( E. x  x  =  ( A  i^i  B )  <->  E. x A. y ( y  e.  x  <->  ( y  e.  A  /\  y  e.  B ) ) )
92, 8mpbir 202 . 2  |-  E. x  x  =  ( A  i^i  B )
109issetri 2734 1  |-  ( A  i^i  B )  e. 
_V
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360   A.wal 1532   E.wex 1537    = wceq 1619    e. wcel 1621   _Vcvv 2727    i^i cin 3077
This theorem is referenced by:  inex2  4053  inex1g  4054  inuni  4071  onfr  4324  ssimaex  5436  exfo  5530  ofmres  5968  fipwuni  7063  fisn  7064  elfiun  7067  dffi3  7068  marypha1lem  7070  epfrs  7297  tcmin  7310  bnd2  7447  kmlem13  7672  brdom3  8037  brdom5  8038  brdom4  8039  fpwwe  8148  canthwelem  8152  pwfseqlem4  8164  ingru  8317  ltweuz  10902  elrest  13206  invfval  13505  isoval  13511  catcval  13772  isacs5lem  14116  isunit  15274  isrhm  15336  2idlval  15817  pjfval  16438  fctop  16573  cctop  16575  ppttop  16576  epttop  16578  mretopd  16661  toponmre  16662  tgrest  16722  resttopon  16724  restco  16727  ordtbas2  16753  cnrest2  16846  cnpresti  16848  cnprest  16849  cnprest2  16850  cmpsublem  16958  cmpsub  16959  consuba  16978  1stcrest  17011  subislly  17039  cldllycmp  17053  lly1stc  17054  txrest  17157  basqtop  17234  fbssfi  17364  trfbas2  17370  snfil  17391  fgcl  17405  filuni  17412  trfil2  17414  cfinfil  17420  csdfil  17421  supfil  17422  zfbas  17423  fin1aufil  17459  fmfnfmlem3  17483  flimrest  17510  hauspwpwf1  17514  fclsrest  17551  tmdgsum2  17611  tsmsval2  17644  tsmssubm  17657  isnmhm  18087  icopnfhmeo  18273  iccpnfhmeo  18275  xrhmeo  18276  pi1buni  18370  minveclem3b  18624  uniioombllem2  18770  uniioombllem6  18775  vitali  18800  ellimc2  19059  limcflf  19063  taylfvallem  19569  taylf  19572  tayl0  19573  taylpfval  19576  xrlimcnp  20095  cvmsss2  22976  cvmcov2  22977  dfon2lem4  23310  predasetex  23348  brapply  23651  toplat  24456  inttop2  24681  qusp  24708  selsubf  25156  selsubf3  25157  pgapspf2  25219  neibastop1  25474  filnetlem3  25495  heiborlem3  25703  heibor  25711  fnwe2lem2  26314  onfrALTlem5  27000  onfrALTlem5VD  27351  polvalN  28783
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4038
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-in 3085
  Copyright terms: Public domain W3C validator