Definition df-rex 1626

Description: Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22.

Assertion

Ref	Expression
df-rex	|- (E.x e. A ph <-> E.x(x e. A /\ ph))

Detailed syntax breakdown of Definition df-rex

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 set x
3		cA	. . 3 class A
4	1, 2, 3	wrex 1622	. 2 wff E.x e. A ph
5	2	cv 1098	. . . . 5 class x
6	5, 3	wcel 1105	. . . 4 wff x e. A
7	6, 1	wa 223	. . 3 wff (x e. A /\ ph)
8	7, 2	wex 956	. 2 wff E.x(x e. A /\ ph)
9	4, 8	wb 146	1 wff (E.x e. A ph <-> E.x(x e. A /\ ph))

This definition is referenced by:  ralnex 1629  rexnal 1630  rexbida 1634  rexbidv2 1642  rexbii2 1648  risset 1661  hbrex 1664  hbre1 1665  r2ex 1667  rexex 1669  ra4e 1671  r19.22 1707  r19.22i2 1709  r19.22dv2 1712  r19.23v 1717  r19.23ai 1718  r19.23ad 1721  r19.29 1732  r19.41v 1739  r19.43 1741  reeanv 1754  rexeq1f 1760  cbvrex 1774  rexv 1796  rcla4e 1845  ceqsrexv 1861  reurex 1899  reu5 1900  reu2 1901  reu3 1902  reu6 1903  2reuswap 1908  reuss2 2246  reuun2 2249  reupick 2250  rabn0 2263  rab0 2264  r19.2z 2318  dfuni2 2473  eluni2 2475  elunirab 2482  iunconst 2540  dfiun2g 2554  dfiin2 2556  iunss 2559  ssiun 2560  iinss 2568  iunid 2571  iunn0 2575  iunxsn 2580  iunxun 2582  iununi 2584  intexrab 2700  onminex 2983  nnsuc 3111  elxp2 3166  dmuni 3276  rnopab2 3310  dfima2 3356  dfima3 3357  elima2 3360  imasng 3375  rnuni 3408  rninxp 3428  imaco 3443  zfrep6 3554  fv2 3659  fnrnfv 3698  dffo4 3759  dffo5 3760  abrexexlem1 3797  imaiun 3803  abexssex 3811  abexex 3812  isomin 3838  iinon 3849  tfrlem8 3857  rdglim2 3888  oarec 4134  elqs 4228  qsexg 4232  snec 4234  mapsn 4283  mapsnen 4364  pssnn 4465  ssnn 4466  unblem2 4470  unfilem1 4476  zfregcl 4519  axinf2 4548  zfinf 4550  r1pwcl 4611  rankuni 4622  scott0 4641  cp 4646  bnd2 4648  aceq1 4653  aceq5lem2 4660  aceq5lem3 4661  aceq6b 4666  ac6lem 4678  kmlem3 4691  kmlem6 4694  kmlem8 4696  kmlem14 4702  zorn2lem6 4717  zorn2lem7 4718  alephval3 4826  cfub 4831  ltexpi 4952  prnmax 5022  genpcl 5034  1pr 5040  ltexprlem5 5069  reclem2pr 5080  suplem1pr 5084  axrnegex 5206  axrrecex 5207  pre-axsup 5214  renegcl 5339  0re 5363  ssxr 5464  redivcl 5705  sup2 5949  infm3 5952  infmsup 5966  nnunb 5968  xrsupsslem 5974  xrinfmsslem 5975  supxrre 5981  2rexuz 6329  nnwof 6342  nnwos 6343  creur 6624  creui 6625  replimt 6643  infcvglem1 7107  ivthlem3 7169  ivthlem7 7173  ivthlem7OLD 7182  infxpidmlem9 7454  infxpidmlem10 7455  isbasis2g 7505  tgval2t 7510  tgval3t 7518  tgss3t 7531  basgent 7533  cncfmet 7792  bcthlem8 7888  bcthlem14 7894  ubthlem6 8400  grothinf 8633  grothprim 8635  cbvrexf 8698  abfi 8708  ficli 8727  hmeogrp 8776  chsscm 9263  chcmh 9264  shless 9476  shne0 9500  nmcopexlem1 10080  nmcfnexlem1 10109  cnlnssadj 10142

Copyright terms: Public domain