Theorem inex1 4578

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 4562	. . 3 |- E. x A. y ( y e. x <-> ( y e. A /\ y e. B ) )
3		dfcleq 2447	. . . . 5 |- ( x = ( A i^i B ) <-> A. y ( y e. x <-> y e. ( A i^i B ) ) )
4		elin 3673	. . . . . . 7 |- ( y e. ( A i^i B ) <-> ( y e. A /\ y e. B ) )
5	4	bibi2i 311	. . . . . 6 |- ( ( y e. x <-> y e. ( A i^i B ) ) <-> ( y e. x <-> ( y e. A /\ y e. B ) ) )
6	5	albii 1645	. . . . 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 249	. . . 4 |- ( x = ( A i^i B ) <-> A. y ( y e. x <-> ( y e. A /\ y e. B ) ) )
8	7	exbii 1672	. . 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 209	. 2 |- E. x x = ( A i^i B )
10	9	issetri 3113	1 |- ( A i^i B ) e. _V

Syntax hints:   <-> wb 184   /\ wa 367   A.wal 1396   = wceq 1398   E.wex 1617   e. wcel 1823   _Vcvv 3106   i^i cin 3460

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-in 3468

This theorem is referenced by:  inex2  4579  inex1g  4580  inuni  4599  onfr  4906  ssimaex  5913  exfo  6025  ofmres  6769  fipwuni  7878  fisn  7879  elfiun  7882  dffi3  7883  marypha1lem  7885  epfrs  8153  tcmin  8163  bnd2  8302  kmlem13  8533  brdom3  8897  brdom5  8898  brdom4  8899  fpwwe  9013  canthwelem  9017  pwfseqlem4  9029  ingru  9182  ltweuz  12054  elrest  14917  invfval  15247  isoval  15253  isofn  15263  zerooval  15477  catcval  15574  isacs5lem  15998  isunit  17501  isrhm  17565  2idlval  18076  pjfval  18910  fctop  19672  cctop  19674  ppttop  19675  epttop  19677  mretopd  19760  toponmre  19761  tgrest  19827  resttopon  19829  restco  19832  ordtbas2  19859  cnrest2  19954  cnpresti  19956  cnprest  19957  cnprest2  19958  cmpsublem  20066  cmpsub  20067  consuba  20087  1stcrest  20120  subislly  20148  cldllycmp  20162  lly1stc  20163  txrest  20298  basqtop  20378  fbssfi  20504  trfbas2  20510  snfil  20531  fgcl  20545  trfil2  20554  cfinfil  20560  csdfil  20561  supfil  20562  zfbas  20563  fin1aufil  20599  fmfnfmlem3  20623  flimrest  20650  hauspwpwf1  20654  fclsrest  20691  tmdgsum2  20761  tsmsval2  20794  tsmssubm  20810  ustuqtop2  20911  metustfbasOLD  21234  metustfbas  21235  restmetu  21256  isnmhm  21419  icopnfhmeo  21609  iccpnfhmeo  21611  xrhmeo  21612  pi1buni  21706  minveclem3b  22009  uniioombllem2  22158  uniioombllem6  22163  vitali  22188  ellimc2  22447  limcflf  22451  taylfvallem  22919  taylf  22922  tayl0  22923  taylpfval  22926  xrlimcnp  23496  maprnin  27785  ordtprsval  28135  ordtprsuni  28136  ordtrestNEW  28138  ordtrest2NEWlem  28139  ordtrest2NEW  28140  ordtconlem1  28141  xrge0iifhmeo  28153  eulerpartgbij  28575  eulerpartlemmf  28578  eulerpart  28585  ballotlemfrc  28729  cvmsss2  28983  cvmcov2  28984  mvrsval  29129  mpstval  29159  mclsind  29194  mthmpps  29206  dfon2lem4  29458  predasetex  29500  brapply  29816  ptrest  30288  neibastop1  30417  filnetlem3  30438  heiborlem3  30549  heibor  30557  fnwe2lem2  31236  fourierdlem48  32176  fourierdlem49  32177  rhmfn  32978  rhmval  32979  rngcvalALTV  33023  ringcvalALTV  33069  rhmsubclem1  33148  rhmsubcALTVlem1  33167  onfrALTlem5  33708  onfrALTlem5VD  34086  polvalN  36026  superficl  38165  ssficl  38167  trficl  38186