Theorem inex1 4543

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 4526	. . 3 |- E. x A. y ( y e. x <-> ( y e. A /\ y e. B ) )
3		dfcleq 2444	. . . . 5 |- ( x = ( A i^i B ) <-> A. y ( y e. x <-> y e. ( A i^i B ) ) )
4		elin 3616	. . . . . . 7 |- ( y e. ( A i^i B ) <-> ( y e. A /\ y e. B ) )
5	4	bibi2i 315	. . . . . 6 |- ( ( y e. x <-> y e. ( A i^i B ) ) <-> ( y e. x <-> ( y e. A /\ y e. B ) ) )
6	5	albii 1690	. . . . 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 253	. . . 4 |- ( x = ( A i^i B ) <-> A. y ( y e. x <-> ( y e. A /\ y e. B ) ) )
8	7	exbii 1717	. . 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 213	. 2 |- E. x x = ( A i^i B )
10	9	issetri 3051	1 |- ( A i^i B ) e. _V

Syntax hints:   <-> wb 188   /\ wa 371   A.wal 1441   = wceq 1443   E.wex 1662   e. wcel 1886   _Vcvv 3044   i^i cin 3402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-v 3046  df-in 3410

This theorem is referenced by:  inex2  4544  inex1g  4545  inuni  4564  predasetex  5394  onfr  5461  ssimaex  5928  exfo  6038  ofmres  6786  fipwuni  7937  fisn  7938  elfiun  7941  dffi3  7942  marypha1lem  7944  epfrs  8212  tcmin  8222  bnd2  8361  kmlem13  8589  brdom3  8953  brdom5  8954  brdom4  8955  fpwwe  9068  canthwelem  9072  pwfseqlem4  9084  ingru  9237  ltweuz  12172  elrest  15319  invfval  15657  isoval  15663  isofn  15673  zerooval  15887  catcval  15984  isacs5lem  16408  isunit  17878  isrhm  17942  2idlval  18450  pjfval  19262  fctop  20012  cctop  20014  ppttop  20015  epttop  20017  mretopd  20101  toponmre  20102  tgrest  20168  resttopon  20170  restco  20173  ordtbas2  20200  cnrest2  20295  cnpresti  20297  cnprest  20298  cnprest2  20299  cmpsublem  20407  cmpsub  20408  consuba  20428  1stcrest  20461  subislly  20489  cldllycmp  20503  lly1stc  20504  txrest  20639  basqtop  20719  fbssfi  20845  trfbas2  20851  snfil  20872  fgcl  20886  trfil2  20895  cfinfil  20901  csdfil  20902  supfil  20903  zfbas  20904  fin1aufil  20940  fmfnfmlem3  20964  flimrest  20991  hauspwpwf1  20995  fclsrest  21032  tmdgsum2  21104  tsmsval2  21137  tsmssubm  21150  ustuqtop2  21250  metustfbas  21565  restmetu  21578  isnmhm  21760  icopnfhmeo  21964  iccpnfhmeo  21966  xrhmeo  21967  pi1buni  22064  minveclem3b  22363  minveclem3bOLD  22375  uniioombllem2  22533  uniioombllem2OLD  22534  uniioombllem6  22539  vitali  22564  ellimc2  22825  limcflf  22829  taylfvallem  23306  taylf  23309  tayl0  23310  taylpfval  23313  xrlimcnp  23887  maprnin  28309  ordtprsval  28717  ordtprsuni  28718  ordtrestNEW  28720  ordtrest2NEWlem  28721  ordtrest2NEW  28722  ordtconlem1  28723  xrge0iifhmeo  28735  eulerpartgbij  29198  eulerpartlemmf  29201  eulerpart  29208  ballotlemfrc  29352  ballotlemfrcOLD  29390  cvmsss2  29990  cvmcov2  29991  mvrsval  30136  mpstval  30166  mclsind  30201  mthmpps  30213  dfon2lem4  30425  brapply  30698  neibastop1  31008  filnetlem3  31029  ptrest  31932  heiborlem3  32138  heibor  32146  polvalN  33464  fnwe2lem2  35903  superficl  36165  ssficl  36167  trficl  36255  onfrALTlem5  36902  onfrALTlem5VD  37276  fourierdlem48  38012  fourierdlem49  38013  sge0resplit  38242  hoiqssbllem3  38440  ewlkle  39606  upgrewlkle2  39608  1wlk1walk  39630  rhmfn  39905  rhmval  39906  rngcvalALTV  39950  ringcvalALTV  39996  rhmsubclem1  40075  rhmsubcALTVlem1  40094