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

Theorem inex1 4236
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 4224 . . 3  |-  E. x A. y ( y  e.  x  <->  ( y  e.  A  /\  y  e.  B ) )
3 dfcleq 2352 . . . . 5  |-  ( x  =  ( A  i^i  B )  <->  A. y ( y  e.  x  <->  y  e.  ( A  i^i  B ) ) )
4 elin 3434 . . . . . . 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 1566 . . . . 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 1582 . . 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 2871 1  |-  ( A  i^i  B )  e. 
_V
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   A.wal 1540   E.wex 1541    = wceq 1642    e. wcel 1710   _Vcvv 2864    i^i cin 3227
This theorem is referenced by:  inex2  4237  inex1g  4238  inuni  4254  onfr  4513  ssimaex  5667  exfo  5761  ofmres  6203  fipwuni  7269  fisn  7270  elfiun  7273  dffi3  7274  marypha1lem  7276  epfrs  7503  tcmin  7516  bnd2  7653  kmlem13  7878  brdom3  8243  brdom5  8244  brdom4  8245  fpwwe  8358  canthwelem  8362  pwfseqlem4  8374  ingru  8527  ltweuz  11116  elrest  13431  invfval  13760  isoval  13766  catcval  14027  isacs5lem  14371  isunit  15538  isrhm  15600  2idlval  16084  pjfval  16712  fctop  16847  cctop  16849  ppttop  16850  epttop  16852  mretopd  16935  toponmre  16936  tgrest  16996  resttopon  16998  restco  17001  ordtbas2  17027  cnrest2  17120  cnpresti  17122  cnprest  17123  cnprest2  17124  cmpsublem  17232  cmpsub  17233  consuba  17252  1stcrest  17285  subislly  17313  cldllycmp  17327  lly1stc  17328  txrest  17431  basqtop  17508  fbssfi  17634  trfbas2  17640  snfil  17661  fgcl  17675  filuni  17682  trfil2  17684  cfinfil  17690  csdfil  17691  supfil  17692  zfbas  17693  fin1aufil  17729  fmfnfmlem3  17753  flimrest  17780  hauspwpwf1  17784  fclsrest  17821  tmdgsum2  17881  tsmsval2  17914  tsmssubm  17927  isnmhm  18357  icopnfhmeo  18545  iccpnfhmeo  18547  xrhmeo  18548  pi1buni  18642  minveclem3b  18896  uniioombllem2  19042  uniioombllem6  19047  vitali  19072  ellimc2  19331  limcflf  19335  taylfvallem  19841  taylf  19844  tayl0  19845  taylpfval  19848  xrlimcnp  20374  xrge0iifhmeo  23478  metustfbas  23601  restmetu  23615  ballotlemfrc  24033  cvmsss2  24209  cvmcov2  24210  dfon2lem4  24700  predasetex  24738  brapply  25035  neibastop1  25632  filnetlem3  25653  heiborlem3  25860  heibor  25868  fnwe2lem2  26471  onfrALTlem5  28052  onfrALTlem5VD  28423  polvalN  30163
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-v 2866  df-in 3235
  Copyright terms: Public domain W3C validator