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

Theorem inex1 4155
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 4143 . . 3  |-  E. x A. y ( y  e.  x  <->  ( y  e.  A  /\  y  e.  B ) )
3 dfcleq 2277 . . . . 5  |-  ( x  =  ( A  i^i  B )  <->  A. y ( y  e.  x  <->  y  e.  ( A  i^i  B ) ) )
4 elin 3358 . . . . . . 7  |-  ( y  e.  ( A  i^i  B )  <->  ( y  e.  A  /\  y  e.  B ) )
54bibi2i 304 . . . . . 6  |-  ( ( y  e.  x  <->  y  e.  ( A  i^i  B ) )  <->  ( y  e.  x  <->  ( y  e.  A  /\  y  e.  B ) ) )
65albii 1553 . . . . 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 240 . . . 4  |-  ( x  =  ( A  i^i  B )  <->  A. y ( y  e.  x  <->  ( y  e.  A  /\  y  e.  B ) ) )
87exbii 1569 . . 3  |-  ( E. x  x  =  ( A  i^i  B )  <->  E. x A. y ( y  e.  x  <->  ( y  e.  A  /\  y  e.  B ) ) )
92, 8mpbir 200 . 2  |-  E. x  x  =  ( A  i^i  B )
109issetri 2795 1  |-  ( A  i^i  B )  e. 
_V
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   A.wal 1527   E.wex 1528    = wceq 1623    e. wcel 1684   _Vcvv 2788    i^i cin 3151
This theorem is referenced by:  inex2  4156  inex1g  4157  inuni  4173  onfr  4431  ssimaex  5584  exfo  5678  ofmres  6116  fipwuni  7179  fisn  7180  elfiun  7183  dffi3  7184  marypha1lem  7186  epfrs  7413  tcmin  7426  bnd2  7563  kmlem13  7788  brdom3  8153  brdom5  8154  brdom4  8155  fpwwe  8268  canthwelem  8272  pwfseqlem4  8284  ingru  8437  ltweuz  11024  elrest  13332  invfval  13661  isoval  13667  catcval  13928  isacs5lem  14272  isunit  15439  isrhm  15501  2idlval  15985  pjfval  16606  fctop  16741  cctop  16743  ppttop  16744  epttop  16746  mretopd  16829  toponmre  16830  tgrest  16890  resttopon  16892  restco  16895  ordtbas2  16921  cnrest2  17014  cnpresti  17016  cnprest  17017  cnprest2  17018  cmpsublem  17126  cmpsub  17127  consuba  17146  1stcrest  17179  subislly  17207  cldllycmp  17221  lly1stc  17222  txrest  17325  basqtop  17402  fbssfi  17532  trfbas2  17538  snfil  17559  fgcl  17573  filuni  17580  trfil2  17582  cfinfil  17588  csdfil  17589  supfil  17590  zfbas  17591  fin1aufil  17627  fmfnfmlem3  17651  flimrest  17678  hauspwpwf1  17682  fclsrest  17719  tmdgsum2  17779  tsmsval2  17812  tsmssubm  17825  isnmhm  18255  icopnfhmeo  18441  iccpnfhmeo  18443  xrhmeo  18444  pi1buni  18538  minveclem3b  18792  uniioombllem2  18938  uniioombllem6  18943  vitali  18968  ellimc2  19227  limcflf  19231  taylfvallem  19737  taylf  19740  tayl0  19741  taylpfval  19744  xrlimcnp  20263  ballotlemfrc  23085  xrge0iifhmeo  23318  cvmsss2  23805  cvmcov2  23806  dfon2lem4  24142  predasetex  24180  brapply  24477  toplat  25290  inttop2  25515  qusp  25542  selsubf  25990  selsubf3  25991  pgapspf2  26053  neibastop1  26308  filnetlem3  26329  heiborlem3  26537  heibor  26545  fnwe2lem2  27148  onfrALTlem5  28307  onfrALTlem5VD  28661  polvalN  30094
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159
  Copyright terms: Public domain W3C validator