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

Theorem inex1 4115
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 4103 . . 3  |-  E. x A. y ( y  e.  x  <->  ( y  e.  A  /\  y  e.  B ) )
3 dfcleq 2250 . . . . 5  |-  ( x  =  ( A  i^i  B )  <->  A. y ( y  e.  x  <->  y  e.  ( A  i^i  B ) ) )
4 elin 3319 . . . . . . 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 2764 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 2757    i^i cin 3112
This theorem is referenced by:  inex2  4116  inex1g  4117  inuni  4135  onfr  4389  ssimaex  5504  exfo  5598  ofmres  6036  fipwuni  7133  fisn  7134  elfiun  7137  dffi3  7138  marypha1lem  7140  epfrs  7367  tcmin  7380  bnd2  7517  kmlem13  7742  brdom3  8107  brdom5  8108  brdom4  8109  fpwwe  8222  canthwelem  8226  pwfseqlem4  8238  ingru  8391  ltweuz  10976  elrest  13280  invfval  13609  isoval  13615  catcval  13876  isacs5lem  14220  isunit  15387  isrhm  15449  2idlval  15933  pjfval  16554  fctop  16689  cctop  16691  ppttop  16692  epttop  16694  mretopd  16777  toponmre  16778  tgrest  16838  resttopon  16840  restco  16843  ordtbas2  16869  cnrest2  16962  cnpresti  16964  cnprest  16965  cnprest2  16966  cmpsublem  17074  cmpsub  17075  consuba  17094  1stcrest  17127  subislly  17155  cldllycmp  17169  lly1stc  17170  txrest  17273  basqtop  17350  fbssfi  17480  trfbas2  17486  snfil  17507  fgcl  17521  filuni  17528  trfil2  17530  cfinfil  17536  csdfil  17537  supfil  17538  zfbas  17539  fin1aufil  17575  fmfnfmlem3  17599  flimrest  17626  hauspwpwf1  17630  fclsrest  17667  tmdgsum2  17727  tsmsval2  17760  tsmssubm  17773  isnmhm  18203  icopnfhmeo  18389  iccpnfhmeo  18391  xrhmeo  18392  pi1buni  18486  minveclem3b  18740  uniioombllem2  18886  uniioombllem6  18891  vitali  18916  ellimc2  19175  limcflf  19179  taylfvallem  19685  taylf  19688  tayl0  19689  taylpfval  19692  xrlimcnp  20211  ballotlemfrc  23032  cvmsss2  23163  cvmcov2  23164  dfon2lem4  23497  predasetex  23535  brapply  23838  toplat  24643  inttop2  24868  qusp  24895  selsubf  25343  selsubf3  25344  pgapspf2  25406  neibastop1  25661  filnetlem3  25682  heiborlem3  25890  heibor  25898  fnwe2lem2  26501  onfrALTlem5  27344  onfrALTlem5VD  27695  polvalN  29245
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 1927  ax-ext 2237  ax-sep 4101
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 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2759  df-in 3120
  Copyright terms: Public domain W3C validator