Theorem inex1 4544

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 2447	. . . . 5 |- ( x = ( A i^i B ) <-> A. y ( y e. x <-> y e. ( A i^i B ) ) )
4		elin 3650	. . . . . . 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 1611	. . . . 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 1635	. . 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 3085	1 |- ( A i^i B ) e. _V

Syntax hints:   <-> wb 184   /\ wa 369   A.wal 1368   = wceq 1370   E.wex 1587   e. wcel 1758   _Vcvv 3078   i^i cin 3438

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4524

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-in 3446

This theorem is referenced by:  inex2  4545  inex1g  4546  inuni  4565  onfr  4869  ssimaex  5868  exfo  5973  ofmres  6686  fipwuni  7790  fisn  7791  elfiun  7794  dffi3  7795  marypha1lem  7797  epfrs  8065  tcmin  8075  bnd2  8214  kmlem13  8445  brdom3  8809  brdom5  8810  brdom4  8811  fpwwe  8927  canthwelem  8931  pwfseqlem4  8943  ingru  9096  ltweuz  11904  elrest  14488  invfval  14819  isoval  14825  catcval  15086  isacs5lem  15461  isunit  16875  isrhm  16937  2idlval  17441  pjfval  18259  fctop  18743  cctop  18745  ppttop  18746  epttop  18748  mretopd  18831  toponmre  18832  tgrest  18898  resttopon  18900  restco  18903  ordtbas2  18930  cnrest2  19025  cnpresti  19027  cnprest  19028  cnprest2  19029  cmpsublem  19137  cmpsub  19138  consuba  19159  1stcrest  19192  subislly  19220  cldllycmp  19234  lly1stc  19235  txrest  19339  basqtop  19419  fbssfi  19545  trfbas2  19551  snfil  19572  fgcl  19586  trfil2  19595  cfinfil  19601  csdfil  19602  supfil  19603  zfbas  19604  fin1aufil  19640  fmfnfmlem3  19664  flimrest  19691  hauspwpwf1  19695  fclsrest  19732  tmdgsum2  19802  tsmsval2  19835  tsmssubm  19851  ustuqtop2  19952  metustfbasOLD  20275  metustfbas  20276  restmetu  20297  isnmhm  20460  icopnfhmeo  20650  iccpnfhmeo  20652  xrhmeo  20653  pi1buni  20747  minveclem3b  21050  uniioombllem2  21199  uniioombllem6  21204  vitali  21229  ellimc2  21488  limcflf  21492  taylfvallem  21959  taylf  21962  tayl0  21963  taylpfval  21966  xrlimcnp  22498  maprnin  26202  ordtprsval  26513  ordtprsuni  26514  ordtrestNEW  26516  ordtrest2NEWlem  26517  ordtrest2NEW  26518  ordtconlem1  26519  xrge0iifhmeo  26531  eulerpartgbij  26919  eulerpartlemmf  26922  eulerpart  26929  ballotlemfrc  27073  cvmsss2  27327  cvmcov2  27328  dfon2lem4  27763  predasetex  27805  brapply  28133  ptrest  28593  neibastop1  28748  filnetlem3  28769  heiborlem3  28880  heibor  28888  fnwe2lem2  29572  onfrALTlem5  31602  onfrALTlem5VD  31973  polvalN  33907