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

Theorem inex1 4156
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 4144 . . 3  |-  E. x A. y ( y  e.  x  <->  ( y  e.  A  /\  y  e.  B ) )
3 dfcleq 2278 . . . . 5  |-  ( x  =  ( A  i^i  B )  <->  A. y ( y  e.  x  <->  y  e.  ( A  i^i  B ) ) )
4 elin 3359 . . . . . . 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 1558 . . . . 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 1574 . . 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 2796 1  |-  ( A  i^i  B )  e. 
_V
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360   A.wal 1532   E.wex 1533    = wceq 1628    e. wcel 1688   _Vcvv 2789    i^i cin 3152
This theorem is referenced by:  inex2  4157  inex1g  4158  inuni  4176  onfr  4430  ssimaex  5545  exfo  5639  ofmres  6077  fipwuni  7174  fisn  7175  elfiun  7178  dffi3  7179  marypha1lem  7181  epfrs  7408  tcmin  7421  bnd2  7558  kmlem13  7783  brdom3  8148  brdom5  8149  brdom4  8150  fpwwe  8263  canthwelem  8267  pwfseqlem4  8279  ingru  8432  ltweuz  11018  elrest  13326  invfval  13655  isoval  13661  catcval  13922  isacs5lem  14266  isunit  15433  isrhm  15495  2idlval  15979  pjfval  16600  fctop  16735  cctop  16737  ppttop  16738  epttop  16740  mretopd  16823  toponmre  16824  tgrest  16884  resttopon  16886  restco  16889  ordtbas2  16915  cnrest2  17008  cnpresti  17010  cnprest  17011  cnprest2  17012  cmpsublem  17120  cmpsub  17121  consuba  17140  1stcrest  17173  subislly  17201  cldllycmp  17215  lly1stc  17216  txrest  17319  basqtop  17396  fbssfi  17526  trfbas2  17532  snfil  17553  fgcl  17567  filuni  17574  trfil2  17576  cfinfil  17582  csdfil  17583  supfil  17584  zfbas  17585  fin1aufil  17621  fmfnfmlem3  17645  flimrest  17672  hauspwpwf1  17676  fclsrest  17713  tmdgsum2  17773  tsmsval2  17806  tsmssubm  17819  isnmhm  18249  icopnfhmeo  18435  iccpnfhmeo  18437  xrhmeo  18438  pi1buni  18532  minveclem3b  18786  uniioombllem2  18932  uniioombllem6  18937  vitali  18962  ellimc2  19221  limcflf  19225  taylfvallem  19731  taylf  19734  tayl0  19735  taylpfval  19738  xrlimcnp  20257  ballotlemfrc  23078  cvmsss2  23209  cvmcov2  23210  dfon2lem4  23543  predasetex  23581  brapply  23884  toplat  24689  inttop2  24914  qusp  24941  selsubf  25389  selsubf3  25390  pgapspf2  25452  neibastop1  25707  filnetlem3  25728  heiborlem3  25936  heibor  25944  fnwe2lem2  26547  onfrALTlem5  27578  onfrALTlem5VD  27929  polvalN  29361
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265  ax-sep 4142
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-in 3160
  Copyright terms: Public domain W3C validator