Theorem inex1 4428

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 4410	. . 3 |- E. x A. y ( y e. x <-> ( y e. A /\ y e. B ) )
3		dfcleq 2432	. . . . 5 |- ( x = ( A i^i B ) <-> A. y ( y e. x <-> y e. ( A i^i B ) ) )
4		elin 3534	. . . . . . 7 |- ( y e. ( A i^i B ) <-> ( y e. A /\ y e. B ) )
5	4	bibi2i 313	. . . . . 6 |- ( ( y e. x <-> y e. ( A i^i B ) ) <-> ( y e. x <-> ( y e. A /\ y e. B ) ) )
6	5	albii 1610	. . . . 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 1634	. . 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 2974	1 |- ( A i^i B ) e. _V

Syntax hints:   <-> wb 184   /\ wa 369   A.wal 1367   = wceq 1369   E.wex 1586   e. wcel 1756   _Vcvv 2967   i^i cin 3322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-in 3330

This theorem is referenced by:  inex2  4429  inex1g  4430  inuni  4449  onfr  4753  ssimaex  5751  exfo  5856  ofmres  6568  fipwuni  7668  fisn  7669  elfiun  7672  dffi3  7673  marypha1lem  7675  epfrs  7943  tcmin  7953  bnd2  8092  kmlem13  8323  brdom3  8687  brdom5  8688  brdom4  8689  fpwwe  8805  canthwelem  8809  pwfseqlem4  8821  ingru  8974  ltweuz  11776  elrest  14358  invfval  14689  isoval  14695  catcval  14956  isacs5lem  15331  isunit  16737  isrhm  16799  2idlval  17292  pjfval  18106  fctop  18583  cctop  18585  ppttop  18586  epttop  18588  mretopd  18671  toponmre  18672  tgrest  18738  resttopon  18740  restco  18743  ordtbas2  18770  cnrest2  18865  cnpresti  18867  cnprest  18868  cnprest2  18869  cmpsublem  18977  cmpsub  18978  consuba  18999  1stcrest  19032  subislly  19060  cldllycmp  19074  lly1stc  19075  txrest  19179  basqtop  19259  fbssfi  19385  trfbas2  19391  snfil  19412  fgcl  19426  trfil2  19435  cfinfil  19441  csdfil  19442  supfil  19443  zfbas  19444  fin1aufil  19480  fmfnfmlem3  19504  flimrest  19531  hauspwpwf1  19535  fclsrest  19572  tmdgsum2  19642  tsmsval2  19675  tsmssubm  19691  ustuqtop2  19792  metustfbasOLD  20115  metustfbas  20116  restmetu  20137  isnmhm  20300  icopnfhmeo  20490  iccpnfhmeo  20492  xrhmeo  20493  pi1buni  20587  minveclem3b  20890  uniioombllem2  21038  uniioombllem6  21043  vitali  21068  ellimc2  21327  limcflf  21331  taylfvallem  21798  taylf  21801  tayl0  21802  taylpfval  21805  xrlimcnp  22337  maprnin  25982  ordtprsval  26300  ordtprsuni  26301  ordtrestNEW  26303  ordtrest2NEWlem  26304  ordtrest2NEW  26305  ordtconlem1  26306  xrge0iifhmeo  26318  eulerpartgbij  26707  eulerpartlemmf  26710  eulerpart  26717  ballotlemfrc  26861  cvmsss2  27115  cvmcov2  27116  dfon2lem4  27550  predasetex  27592  brapply  27920  ptrest  28378  neibastop1  28533  filnetlem3  28554  heiborlem3  28665  heibor  28673  fnwe2lem2  29357  onfrALTlem5  31137  onfrALTlem5VD  31508  polvalN  33389