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

Theorem inex1 4346
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
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 inex1.1 . . . 4  |-  A  e. 
_V
21zfauscl 4334 . . 3  |-  E. x A. y ( y  e.  x  <->  ( y  e.  A  /\  y  e.  B ) )
3 dfcleq 2432 . . . . 5  |-  ( x  =  ( A  i^i  B )  <->  A. y ( y  e.  x  <->  y  e.  ( A  i^i  B ) ) )
4 elin 3532 . . . . . . 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 1576 . . . . 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 1593 . . 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 2965 1  |-  ( A  i^i  B )  e. 
_V
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360   A.wal 1550   E.wex 1551    = wceq 1653    e. wcel 1726   _Vcvv 2958    i^i cin 3321
This theorem is referenced by:  inex2  4347  inex1g  4348  inuni  4364  onfr  4622  ssimaex  5790  exfo  5889  ofmres  6345  fipwuni  7433  fisn  7434  elfiun  7437  dffi3  7438  marypha1lem  7440  epfrs  7669  tcmin  7682  bnd2  7819  kmlem13  8044  brdom3  8408  brdom5  8409  brdom4  8410  fpwwe  8523  canthwelem  8527  pwfseqlem4  8539  ingru  8692  ltweuz  11303  elrest  13657  invfval  13986  isoval  13992  catcval  14253  isacs5lem  14597  isunit  15764  isrhm  15826  2idlval  16306  pjfval  16935  fctop  17070  cctop  17072  ppttop  17073  epttop  17075  mretopd  17158  toponmre  17159  tgrest  17225  resttopon  17227  restco  17230  ordtbas2  17257  cnrest2  17352  cnpresti  17354  cnprest  17355  cnprest2  17356  cmpsublem  17464  cmpsub  17465  consuba  17485  1stcrest  17518  subislly  17546  cldllycmp  17560  lly1stc  17561  txrest  17665  basqtop  17745  fbssfi  17871  trfbas2  17877  snfil  17898  fgcl  17912  filuni  17919  trfil2  17921  cfinfil  17927  csdfil  17928  supfil  17929  zfbas  17930  fin1aufil  17966  fmfnfmlem3  17990  flimrest  18017  hauspwpwf1  18021  fclsrest  18058  tmdgsum2  18128  tsmsval2  18161  tsmssubm  18174  ustuqtop2  18274  metustfbasOLD  18597  metustfbas  18598  restmetu  18619  isnmhm  18782  icopnfhmeo  18970  iccpnfhmeo  18972  xrhmeo  18973  pi1buni  19067  minveclem3b  19331  uniioombllem2  19477  uniioombllem6  19482  vitali  19507  ellimc2  19766  limcflf  19770  taylfvallem  20276  taylf  20279  tayl0  20280  taylpfval  20283  xrlimcnp  20809  xrge0iifhmeo  24324  ballotlemfrc  24786  cvmsss2  24963  cvmcov2  24964  dfon2lem4  25415  predasetex  25457  brapply  25785  neibastop1  26390  filnetlem3  26411  heiborlem3  26524  heibor  26532  fnwe2lem2  27128  onfrALTlem5  28630  onfrALTlem5VD  28999  polvalN  30704
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-in 3329
  Copyright terms: Public domain W3C validator