Theorem inex1 4588

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 4570	. . 3 |- E. x A. y ( y e. x <-> ( y e. A /\ y e. B ) )
3		dfcleq 2460	. . . . 5 |- ( x = ( A i^i B ) <-> A. y ( y e. x <-> y e. ( A i^i B ) ) )
4		elin 3687	. . . . . . 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 1620	. . . . 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 1644	. . 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 3120	1 |- ( A i^i B ) e. _V

Syntax hints:   <-> wb 184   /\ wa 369   A.wal 1377   = wceq 1379   E.wex 1596   e. wcel 1767   _Vcvv 3113   i^i cin 3475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483

This theorem is referenced by:  inex2  4589  inex1g  4590  inuni  4609  onfr  4917  ssimaex  5931  exfo  6038  ofmres  6780  fipwuni  7885  fisn  7886  elfiun  7889  dffi3  7890  marypha1lem  7892  epfrs  8161  tcmin  8171  bnd2  8310  kmlem13  8541  brdom3  8905  brdom5  8906  brdom4  8907  fpwwe  9023  canthwelem  9027  pwfseqlem4  9039  ingru  9192  ltweuz  12039  elrest  14682  invfval  15013  isoval  15019  catcval  15280  isacs5lem  15655  isunit  17102  isrhm  17166  2idlval  17675  pjfval  18520  fctop  19287  cctop  19289  ppttop  19290  epttop  19292  mretopd  19375  toponmre  19376  tgrest  19442  resttopon  19444  restco  19447  ordtbas2  19474  cnrest2  19569  cnpresti  19571  cnprest  19572  cnprest2  19573  cmpsublem  19681  cmpsub  19682  consuba  19703  1stcrest  19736  subislly  19764  cldllycmp  19778  lly1stc  19779  txrest  19883  basqtop  19963  fbssfi  20089  trfbas2  20095  snfil  20116  fgcl  20130  trfil2  20139  cfinfil  20145  csdfil  20146  supfil  20147  zfbas  20148  fin1aufil  20184  fmfnfmlem3  20208  flimrest  20235  hauspwpwf1  20239  fclsrest  20276  tmdgsum2  20346  tsmsval2  20379  tsmssubm  20395  ustuqtop2  20496  metustfbasOLD  20819  metustfbas  20820  restmetu  20841  isnmhm  21004  icopnfhmeo  21194  iccpnfhmeo  21196  xrhmeo  21197  pi1buni  21291  minveclem3b  21594  uniioombllem2  21743  uniioombllem6  21748  vitali  21773  ellimc2  22032  limcflf  22036  taylfvallem  22503  taylf  22506  tayl0  22507  taylpfval  22510  xrlimcnp  23042  maprnin  27242  ordtprsval  27552  ordtprsuni  27553  ordtrestNEW  27555  ordtrest2NEWlem  27556  ordtrest2NEW  27557  ordtconlem1  27558  xrge0iifhmeo  27570  eulerpartgbij  27967  eulerpartlemmf  27970  eulerpart  27977  ballotlemfrc  28121  cvmsss2  28375  cvmcov2  28376  dfon2lem4  28811  predasetex  28853  brapply  29181  ptrest  29641  neibastop1  29796  filnetlem3  29817  heiborlem3  29928  heibor  29936  fnwe2lem2  30617  onfrALTlem5  32403  onfrALTlem5VD  32774  polvalN  34710  superficl  36781  ssficl  36783  trficl  36798