Theorem inex1 4304

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.

Step	Hyp	Ref	Expression
1		inex1.1	. . . 4 |- A e. _V
2	1	zfauscl 4292	. . 3 |- E. x A. y ( y e. x <-> ( y e. A /\ y e. B ) )
3		dfcleq 2398	. . . . 5 |- ( x = ( A i^i B ) <-> A. y ( y e. x <-> y e. ( A i^i B ) ) )
4		elin 3490	. . . . . . 7 |- ( y e. ( A i^i B ) <-> ( y e. A /\ y e. B ) )
5	4	bibi2i 305	. . . . . 6 |- ( ( y e. x <-> y e. ( A i^i B ) ) <-> ( y e. x <-> ( y e. A /\ y e. B ) ) )
6	5	albii 1572	. . . . 5 |- ( A. y ( y e. x <-> y e. ( A i^i B ) ) <-> A. y ( y e. x <-> ( y e. A /\ y e. B ) ) )
7	3, 6	bitri 241	. . . 4 |- ( x = ( A i^i B ) <-> A. y ( y e. x <-> ( y e. A /\ y e. B ) ) )
8	7	exbii 1589	. . 3 |- ( E. x x = ( A i^i B ) <-> E. x A. y ( y e. x <-> ( y e. A /\ y e. B ) ) )
9	2, 8	mpbir 201	. 2 |- E. x x = ( A i^i B )
10	9	issetri 2923	1 |- ( A i^i B ) e. _V

Syntax hints:   <-> wb 177   /\ wa 359   A.wal 1546   E.wex 1547   = wceq 1649   e. wcel 1721   _Vcvv 2916   i^i cin 3279

This theorem is referenced by:  inex2  4305  inex1g  4306  inuni  4322  onfr  4580  ssimaex  5747  exfo  5846  ofmres  6302  fipwuni  7389  fisn  7390  elfiun  7393  dffi3  7394  marypha1lem  7396  epfrs  7623  tcmin  7636  bnd2  7773  kmlem13  7998  brdom3  8362  brdom5  8363  brdom4  8364  fpwwe  8477  canthwelem  8481  pwfseqlem4  8493  ingru  8646  ltweuz  11256  elrest  13610  invfval  13939  isoval  13945  catcval  14206  isacs5lem  14550  isunit  15717  isrhm  15779  2idlval  16259  pjfval  16888  fctop  17023  cctop  17025  ppttop  17026  epttop  17028  mretopd  17111  toponmre  17112  tgrest  17177  resttopon  17179  restco  17182  ordtbas2  17209  cnrest2  17304  cnpresti  17306  cnprest  17307  cnprest2  17308  cmpsublem  17416  cmpsub  17417  consuba  17436  1stcrest  17469  subislly  17497  cldllycmp  17511  lly1stc  17512  txrest  17616  basqtop  17696  fbssfi  17822  trfbas2  17828  snfil  17849  fgcl  17863  filuni  17870  trfil2  17872  cfinfil  17878  csdfil  17879  supfil  17880  zfbas  17881  fin1aufil  17917  fmfnfmlem3  17941  flimrest  17968  hauspwpwf1  17972  fclsrest  18009  tmdgsum2  18079  tsmsval2  18112  tsmssubm  18125  ustuqtop2  18225  metustfbasOLD  18548  metustfbas  18549  restmetu  18570  isnmhm  18733  icopnfhmeo  18921  iccpnfhmeo  18923  xrhmeo  18924  pi1buni  19018  minveclem3b  19282  uniioombllem2  19428  uniioombllem6  19433  vitali  19458  ellimc2  19717  limcflf  19721  taylfvallem  20227  taylf  20230  tayl0  20231  taylpfval  20234  xrlimcnp  20760  xrge0iifhmeo  24275  ballotlemfrc  24737  cvmsss2  24914  cvmcov2  24915  dfon2lem4  25356  predasetex  25394  brapply  25691  neibastop1  26278  filnetlem3  26299  heiborlem3  26412  heibor  26420  fnwe2lem2  27016  onfrALTlem5  28339  onfrALTlem5VD  28706  polvalN  30387

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287