Theorem inex1 4566

Description: Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22. (Contributed by NM, 21-Jun-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 4550	. . 3 |- E. x A. y ( y e. x <-> ( y e. A /\ y e. B ) )
3		dfcleq 2422	. . . . 5 |- ( x = ( A i^i B ) <-> A. y ( y e. x <-> y e. ( A i^i B ) ) )
4		elin 3655	. . . . . . 7 |- ( y e. ( A i^i B ) <-> ( y e. A /\ y e. B ) )
5	4	bibi2i 314	. . . . . 6 |- ( ( y e. x <-> y e. ( A i^i B ) ) <-> ( y e. x <-> ( y e. A /\ y e. B ) ) )
6	5	albii 1687	. . . . 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 252	. . . 4 |- ( x = ( A i^i B ) <-> A. y ( y e. x <-> ( y e. A /\ y e. B ) ) )
8	7	exbii 1714	. . 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 212	. 2 |- E. x x = ( A i^i B )
10	9	issetri 3094	1 |- ( A i^i B ) e. _V

Syntax hints:   <-> wb 187   /\ wa 370   A.wal 1435   = wceq 1437   E.wex 1659   e. wcel 1870   _Vcvv 3087   i^i cin 3441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-in 3449

This theorem is referenced by:  inex2  4567  inex1g  4568  inuni  4587  predasetex  5414  onfr  5481  ssimaex  5946  exfo  6055  ofmres  6803  fipwuni  7946  fisn  7947  elfiun  7950  dffi3  7951  marypha1lem  7953  epfrs  8214  tcmin  8224  bnd2  8363  kmlem13  8590  brdom3  8954  brdom5  8955  brdom4  8956  fpwwe  9070  canthwelem  9074  pwfseqlem4  9086  ingru  9239  ltweuz  12172  elrest  15285  invfval  15615  isoval  15621  isofn  15631  zerooval  15845  catcval  15942  isacs5lem  16366  isunit  17820  isrhm  17884  2idlval  18392  pjfval  19200  fctop  19950  cctop  19952  ppttop  19953  epttop  19955  mretopd  20039  toponmre  20040  tgrest  20106  resttopon  20108  restco  20111  ordtbas2  20138  cnrest2  20233  cnpresti  20235  cnprest  20236  cnprest2  20237  cmpsublem  20345  cmpsub  20346  consuba  20366  1stcrest  20399  subislly  20427  cldllycmp  20441  lly1stc  20442  txrest  20577  basqtop  20657  fbssfi  20783  trfbas2  20789  snfil  20810  fgcl  20824  trfil2  20833  cfinfil  20839  csdfil  20840  supfil  20841  zfbas  20842  fin1aufil  20878  fmfnfmlem3  20902  flimrest  20929  hauspwpwf1  20933  fclsrest  20970  tmdgsum2  21042  tsmsval2  21075  tsmssubm  21088  ustuqtop2  21188  metustfbas  21503  restmetu  21516  isnmhm  21678  icopnfhmeo  21867  iccpnfhmeo  21869  xrhmeo  21870  pi1buni  21964  minveclem3b  22263  uniioombllem2  22417  uniioombllem2OLD  22418  uniioombllem6  22423  vitali  22448  ellimc2  22709  limcflf  22713  taylfvallem  23178  taylf  23181  tayl0  23182  taylpfval  23185  xrlimcnp  23759  maprnin  28159  ordtprsval  28563  ordtprsuni  28564  ordtrestNEW  28566  ordtrest2NEWlem  28567  ordtrest2NEW  28568  ordtconlem1  28569  xrge0iifhmeo  28581  eulerpartgbij  29031  eulerpartlemmf  29034  eulerpart  29041  ballotlemfrc  29185  cvmsss2  29785  cvmcov2  29786  mvrsval  29931  mpstval  29961  mclsind  29996  mthmpps  30008  dfon2lem4  30219  brapply  30490  neibastop1  30800  filnetlem3  30821  ptrest  31643  heiborlem3  31849  heibor  31857  polvalN  33179  fnwe2lem2  35615  superficl  35870  ssficl  35872  trficl  35900  onfrALTlem5  36545  onfrALTlem5VD  36922  fourierdlem48  37586  fourierdlem49  37587  sge0resplit  37782  rhmfn  38676  rhmval  38677  rngcvalALTV  38721  ringcvalALTV  38767  rhmsubclem1  38846  rhmsubcALTVlem1  38865