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

Theorem inex1 4095
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 4083 . . 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 3300 . . . . . . 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 2747 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 2740    i^i cin 3093
This theorem is referenced by:  inex2  4096  inex1g  4097  inuni  4115  onfr  4368  ssimaex  5483  exfo  5577  ofmres  6015  fipwuni  7112  fisn  7113  elfiun  7116  dffi3  7117  marypha1lem  7119  epfrs  7346  tcmin  7359  bnd2  7496  kmlem13  7721  brdom3  8086  brdom5  8087  brdom4  8088  fpwwe  8201  canthwelem  8205  pwfseqlem4  8217  ingru  8370  ltweuz  10955  elrest  13259  invfval  13588  isoval  13594  catcval  13855  isacs5lem  14199  isunit  15366  isrhm  15428  2idlval  15912  pjfval  16533  fctop  16668  cctop  16670  ppttop  16671  epttop  16673  mretopd  16756  toponmre  16757  tgrest  16817  resttopon  16819  restco  16822  ordtbas2  16848  cnrest2  16941  cnpresti  16943  cnprest  16944  cnprest2  16945  cmpsublem  17053  cmpsub  17054  consuba  17073  1stcrest  17106  subislly  17134  cldllycmp  17148  lly1stc  17149  txrest  17252  basqtop  17329  fbssfi  17459  trfbas2  17465  snfil  17486  fgcl  17500  filuni  17507  trfil2  17509  cfinfil  17515  csdfil  17516  supfil  17517  zfbas  17518  fin1aufil  17554  fmfnfmlem3  17578  flimrest  17605  hauspwpwf1  17609  fclsrest  17646  tmdgsum2  17706  tsmsval2  17739  tsmssubm  17752  isnmhm  18182  icopnfhmeo  18368  iccpnfhmeo  18370  xrhmeo  18371  pi1buni  18465  minveclem3b  18719  uniioombllem2  18865  uniioombllem6  18870  vitali  18895  ellimc2  19154  limcflf  19158  taylfvallem  19664  taylf  19667  tayl0  19668  taylpfval  19671  xrlimcnp  20190  ballotlemfrc  23011  cvmsss2  23142  cvmcov2  23143  dfon2lem4  23476  predasetex  23514  brapply  23817  toplat  24622  inttop2  24847  qusp  24874  selsubf  25322  selsubf3  25323  pgapspf2  25385  neibastop1  25640  filnetlem3  25661  heiborlem3  25869  heibor  25877  fnwe2lem2  26480  onfrALTlem5  27323  onfrALTlem5VD  27674  polvalN  29224
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 4081
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 2742  df-in 3101
  Copyright terms: Public domain W3C validator