Theorem inex1 4593

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

Assertion

Ref	Expression
inex1

Proof of Theorem inex1

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		inex1.1	. . . 4
2	1	zfauscl 4575	. . 3
3		dfcleq 2450	. . . . 5
4		elin 3686	. . . . . . 7
5	4	bibi2i 313	. . . . . 6
6	5	albii 1640	. . . . 5
7	3, 6	bitri 249	. . . 4
8	7	exbii 1667	. . 3
9	2, 8	mpbir 209	. 2
10	9	issetri 3116	1

Syntax hints:  <->wb 184  /\wa 369  A.wal 1393  =wceq 1395  E.wex 1612  e.wcel 1818  cvv 3109  i^icin 3474

This theorem is referenced by:  inex2  4594  inex1g  4595  inuni  4614  onfr  4922  ssimaex  5938  exfo  6049  ofmres  6796  fipwuni  7906  fisn  7907  elfiun  7910  dffi3  7911  marypha1lem  7913  epfrs  8183  tcmin  8193  bnd2  8332  kmlem13  8563  brdom3  8927  brdom5  8928  brdom4  8929  fpwwe  9045  canthwelem  9049  pwfseqlem4  9061  ingru  9214  ltweuz  12072  elrest  14825  invfval  15153  isoval  15159  catcval  15423  isacs5lem  15799  isunit  17306  isrhm  17370  2idlval  17881  pjfval  18737  fctop  19505  cctop  19507  ppttop  19508  epttop  19510  mretopd  19593  toponmre  19594  tgrest  19660  resttopon  19662  restco  19665  ordtbas2  19692  cnrest2  19787  cnpresti  19789  cnprest  19790  cnprest2  19791  cmpsublem  19899  cmpsub  19900  consuba  19921  1stcrest  19954  subislly  19982  cldllycmp  19996  lly1stc  19997  txrest  20132  basqtop  20212  fbssfi  20338  trfbas2  20344  snfil  20365  fgcl  20379  trfil2  20388  cfinfil  20394  csdfil  20395  supfil  20396  zfbas  20397  fin1aufil  20433  fmfnfmlem3  20457  flimrest  20484  hauspwpwf1  20488  fclsrest  20525  tmdgsum2  20595  tsmsval2  20628  tsmssubm  20644  ustuqtop2  20745  metustfbasOLD  21068  metustfbas  21069  restmetu  21090  isnmhm  21253  icopnfhmeo  21443  iccpnfhmeo  21445  xrhmeo  21446  pi1buni  21540  minveclem3b  21843  uniioombllem2  21992  uniioombllem6  21997  vitali  22022  ellimc2  22281  limcflf  22285  taylfvallem  22753  taylf  22756  tayl0  22757  taylpfval  22760  xrlimcnp  23298  maprnin  27554  ordtprsval  27900  ordtprsuni  27901  ordtrestNEW  27903  ordtrest2NEWlem  27904  ordtrest2NEW  27905  ordtconlem1  27906  xrge0iifhmeo  27918  eulerpartgbij  28311  eulerpartlemmf  28314  eulerpart  28321  ballotlemfrc  28465  cvmsss2  28719  cvmcov2  28720  mvrsval  28865  mpstval  28895  mclsind  28930  mthmpps  28942  dfon2lem4  29218  predasetex  29260  brapply  29588  ptrest  30048  neibastop1  30177  filnetlem3  30198  heiborlem3  30309  heibor  30317  fnwe2lem2  30997  fourierdlem48  31937  fourierdlem49  31938  isofn  32567  zerooval  32605  rhmfn  32724  rhmval  32725  rngcvalOLD  32769  ringcvalOLD  32815  rhmsubclem1  32894  rhmsubcOLDlem1  32913  onfrALTlem5  33314  onfrALTlem5VD  33685  polvalN  35629  superficl  37752  ssficl  37754  trficl  37779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482