Theorem inex1 4799

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 4783	. . 3 |- E. x A. y ( y e. x <-> ( y e. A /\ y e. B ) )
3		dfcleq 2616	. . . . 5 |- ( x = ( A i^i B ) <-> A. y ( y e. x <-> y e. ( A i^i B ) ) )
4		elin 3796	. . . . . . 7 |- ( y e. ( A i^i B ) <-> ( y e. A /\ y e. B ) )
5	4	bibi2i 327	. . . . . 6 |- ( ( y e. x <-> y e. ( A i^i B ) ) <-> ( y e. x <-> ( y e. A /\ y e. B ) ) )
6	5	albii 1747	. . . . 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 264	. . . 4 |- ( x = ( A i^i B ) <-> A. y ( y e. x <-> ( y e. A /\ y e. B ) ) )
8	7	exbii 1774	. . 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 221	. 2 |- E. x x = ( A i^i B )
10	9	issetri 3210	1 |- ( A i^i B ) e. _V

Syntax hints:   <-> wb 196   /\ wa 384   A.wal 1481   = wceq 1483   E.wex 1704   e. wcel 1990   _Vcvv 3200   i^i cin 3573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581

This theorem is referenced by:  inex2  4800  inex1g  4801  inuni  4826  predasetex  5695  onfr  5763  ssimaex  6263  exfo  6377  ofmres  7164  fipwuni  8332  fisn  8333  elfiun  8336  dffi3  8337  marypha1lem  8339  epfrs  8607  tcmin  8617  bnd2  8756  kmlem13  8984  brdom3  9350  brdom5  9351  brdom4  9352  fpwwe  9468  canthwelem  9472  pwfseqlem4  9484  ingru  9637  ltweuz  12760  elrest  16088  invfval  16419  isoval  16425  isofn  16435  zerooval  16649  catcval  16746  isacs5lem  17169  isunit  18657  isrhm  18721  2idlval  19233  pjfval  20050  fctop  20808  cctop  20810  ppttop  20811  epttop  20813  mretopd  20896  toponmre  20897  tgrest  20963  resttopon  20965  restco  20968  ordtbas2  20995  cnrest2  21090  cnpresti  21092  cnprest  21093  cnprest2  21094  cmpsublem  21202  cmpsub  21203  connsuba  21223  1stcrest  21256  subislly  21284  cldllycmp  21298  lly1stc  21299  txrest  21434  basqtop  21514  fbssfi  21641  trfbas2  21647  snfil  21668  fgcl  21682  trfil2  21691  cfinfil  21697  csdfil  21698  supfil  21699  zfbas  21700  fin1aufil  21736  fmfnfmlem3  21760  flimrest  21787  hauspwpwf1  21791  fclsrest  21828  tmdgsum2  21900  tsmsval2  21933  tsmssubm  21946  ustuqtop2  22046  metustfbas  22362  restmetu  22375  isnmhm  22550  icopnfhmeo  22742  iccpnfhmeo  22744  xrhmeo  22745  pi1buni  22840  minveclem3b  23199  uniioombllem2  23351  uniioombllem6  23356  vitali  23382  ellimc2  23641  limcflf  23645  taylfvallem  24112  taylf  24115  tayl0  24116  taylpfval  24119  xrlimcnp  24695  ewlkle  26501  upgrewlkle2  26502  wlk1walk  26535  maprnin  29506  ordtprsval  29964  ordtprsuni  29965  ordtrestNEW  29967  ordtrest2NEWlem  29968  ordtrest2NEW  29969  ordtconnlem1  29970  xrge0iifhmeo  29982  eulerpartgbij  30434  eulerpartlemmf  30437  eulerpart  30444  ballotlemfrc  30588  cvmsss2  31256  cvmcov2  31257  mvrsval  31402  mpstval  31432  mclsind  31467  mthmpps  31479  dfon2lem4  31691  brapply  32045  neibastop1  32354  filnetlem3  32375  bj-restn0  33043  bj-restuni  33050  ptrest  33408  heiborlem3  33612  heibor  33620  polvalN  35191  fnwe2lem2  37621  superficl  37872  ssficl  37874  trficl  37961  onfrALTlem5  38757  onfrALTlem5VD  39121  fourierdlem48  40371  fourierdlem49  40372  sge0resplit  40623  hoiqssbllem3  40838  rhmfn  41918  rhmval  41919  rngcvalALTV  41961  ringcvalALTV  42007  rhmsubclem1  42086  rhmsubcALTVlem1  42104