Theorem inex1 4537

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 4520	. . 3 |- E. x A. y ( y e. x <-> ( y e. A /\ y e. B ) )
3		dfcleq 2465	. . . . 5 |- ( x = ( A i^i B ) <-> A. y ( y e. x <-> y e. ( A i^i B ) ) )
4		elin 3608	. . . . . . 7 |- ( y e. ( A i^i B ) <-> ( y e. A /\ y e. B ) )
5	4	bibi2i 320	. . . . . 6 |- ( ( y e. x <-> y e. ( A i^i B ) ) <-> ( y e. x <-> ( y e. A /\ y e. B ) ) )
6	5	albii 1699	. . . . 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 257	. . . 4 |- ( x = ( A i^i B ) <-> A. y ( y e. x <-> ( y e. A /\ y e. B ) ) )
8	7	exbii 1726	. . 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 214	. 2 |- E. x x = ( A i^i B )
10	9	issetri 3038	1 |- ( A i^i B ) e. _V

Syntax hints:   <-> wb 189   /\ wa 376   A.wal 1450   = wceq 1452   E.wex 1671   e. wcel 1904   _Vcvv 3031   i^i cin 3389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-in 3397

This theorem is referenced by:  inex2  4538  inex1g  4539  inuni  4563  predasetex  5402  onfr  5469  ssimaex  5945  exfo  6055  ofmres  6808  fipwuni  7958  fisn  7959  elfiun  7962  dffi3  7963  marypha1lem  7965  epfrs  8233  tcmin  8243  bnd2  8382  kmlem13  8610  brdom3  8974  brdom5  8975  brdom4  8976  fpwwe  9089  canthwelem  9093  pwfseqlem4  9105  ingru  9258  ltweuz  12213  elrest  15404  invfval  15742  isoval  15748  isofn  15758  zerooval  15972  catcval  16069  isacs5lem  16493  isunit  17963  isrhm  18027  2idlval  18534  pjfval  19346  fctop  20096  cctop  20098  ppttop  20099  epttop  20101  mretopd  20185  toponmre  20186  tgrest  20252  resttopon  20254  restco  20257  ordtbas2  20284  cnrest2  20379  cnpresti  20381  cnprest  20382  cnprest2  20383  cmpsublem  20491  cmpsub  20492  consuba  20512  1stcrest  20545  subislly  20573  cldllycmp  20587  lly1stc  20588  txrest  20723  basqtop  20803  fbssfi  20930  trfbas2  20936  snfil  20957  fgcl  20971  trfil2  20980  cfinfil  20986  csdfil  20987  supfil  20988  zfbas  20989  fin1aufil  21025  fmfnfmlem3  21049  flimrest  21076  hauspwpwf1  21080  fclsrest  21117  tmdgsum2  21189  tsmsval2  21222  tsmssubm  21235  ustuqtop2  21335  metustfbas  21650  restmetu  21663  isnmhm  21845  icopnfhmeo  22049  iccpnfhmeo  22051  xrhmeo  22052  pi1buni  22149  minveclem3b  22448  minveclem3bOLD  22460  uniioombllem2  22619  uniioombllem2OLD  22620  uniioombllem6  22625  vitali  22650  ellimc2  22911  limcflf  22915  taylfvallem  23392  taylf  23395  tayl0  23396  taylpfval  23399  xrlimcnp  23973  maprnin  28391  ordtprsval  28798  ordtprsuni  28799  ordtrestNEW  28801  ordtrest2NEWlem  28802  ordtrest2NEW  28803  ordtconlem1  28804  xrge0iifhmeo  28816  eulerpartgbij  29278  eulerpartlemmf  29281  eulerpart  29288  ballotlemfrc  29432  ballotlemfrcOLD  29470  cvmsss2  30069  cvmcov2  30070  mvrsval  30215  mpstval  30245  mclsind  30280  mthmpps  30292  dfon2lem4  30503  brapply  30776  neibastop1  31086  filnetlem3  31107  ptrest  32003  heiborlem3  32209  heibor  32217  polvalN  33541  fnwe2lem2  35980  superficl  36242  ssficl  36244  trficl  36332  onfrALTlem5  36978  onfrALTlem5VD  37345  fourierdlem48  38130  fourierdlem49  38131  sge0resplit  38362  hoiqssbllem3  38564  ewlkle  39811  upgrewlkle2  39812  1wlk1walk  39838  rhmfn  40426  rhmval  40427  rngcvalALTV  40471  ringcvalALTV  40517  rhmsubclem1  40596  rhmsubcALTVlem1  40615