Theorem inex1 4421

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 4403	. . 3 |- E. x A. y ( y e. x <-> ( y e. A /\ y e. B ) )
3		dfcleq 2427	. . . . 5 |- ( x = ( A i^i B ) <-> A. y ( y e. x <-> y e. ( A i^i B ) ) )
4		elin 3527	. . . . . . 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 1613	. . . . 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 2969	1 |- ( A i^i B ) e. _V

Syntax hints:   <-> wb 184   /\ wa 369   A.wal 1360   = wceq 1362   E.wex 1589   e. wcel 1755   _Vcvv 2962   i^i cin 3315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-in 3323

This theorem is referenced by:  inex2  4422  inex1g  4423  inuni  4442  onfr  4745  ssimaex  5744  exfo  5849  ofmres  6562  fipwuni  7664  fisn  7665  elfiun  7668  dffi3  7669  marypha1lem  7671  epfrs  7939  tcmin  7949  bnd2  8088  kmlem13  8319  brdom3  8683  brdom5  8684  brdom4  8685  fpwwe  8801  canthwelem  8805  pwfseqlem4  8817  ingru  8970  ltweuz  11768  elrest  14349  invfval  14680  isoval  14686  catcval  14947  isacs5lem  15322  isunit  16683  isrhm  16745  2idlval  17237  pjfval  17973  fctop  18450  cctop  18452  ppttop  18453  epttop  18455  mretopd  18538  toponmre  18539  tgrest  18605  resttopon  18607  restco  18610  ordtbas2  18637  cnrest2  18732  cnpresti  18734  cnprest  18735  cnprest2  18736  cmpsublem  18844  cmpsub  18845  consuba  18866  1stcrest  18899  subislly  18927  cldllycmp  18941  lly1stc  18942  txrest  19046  basqtop  19126  fbssfi  19252  trfbas2  19258  snfil  19279  fgcl  19293  trfil2  19302  cfinfil  19308  csdfil  19309  supfil  19310  zfbas  19311  fin1aufil  19347  fmfnfmlem3  19371  flimrest  19398  hauspwpwf1  19402  fclsrest  19439  tmdgsum2  19509  tsmsval2  19542  tsmssubm  19558  ustuqtop2  19659  metustfbasOLD  19982  metustfbas  19983  restmetu  20004  isnmhm  20167  icopnfhmeo  20357  iccpnfhmeo  20359  xrhmeo  20360  pi1buni  20454  minveclem3b  20757  uniioombllem2  20905  uniioombllem6  20910  vitali  20935  ellimc2  21194  limcflf  21198  taylfvallem  21708  taylf  21711  tayl0  21712  taylpfval  21715  xrlimcnp  22247  maprnin  25856  ordtprsval  26202  ordtprsuni  26203  ordtrestNEW  26205  ordtrest2NEWlem  26206  ordtrest2NEW  26207  ordtconlem1  26208  xrge0iifhmeo  26220  eulerpartgbij  26603  eulerpartlemmf  26606  eulerpart  26613  ballotlemfrc  26757  cvmsss2  27011  cvmcov2  27012  dfon2lem4  27446  predasetex  27488  brapply  27816  ptrest  28269  neibastop1  28424  filnetlem3  28445  heiborlem3  28556  heibor  28564  fnwe2lem2  29249  onfrALTlem5  30951  onfrALTlem5VD  31323  polvalN  33122