Definition df-rex 1650

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 1646	. 2 wff E.x e. A ph
5	2	cv 955	. . . . 5 class x
6	5, 3	wcel 958	. . . 4 wff x e. A
7	6, 1	wa 223	. . 3 wff (x e. A /\ ph)
8	7, 2	wex 980	. 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 1653  rexnal 1654  rexbida 1658  rexbidv2 1666  rexbii2 1672  risset 1685  hbrex 1688  hbre1 1689  r2ex 1691  rexex 1693  ra4e 1695  r19.22 1731  r19.22i2 1733  r19.22dv2 1736  r19.23v 1741  r19.23ai 1742  r19.23ad 1745  r19.29 1756  r19.41v 1763  r19.43 1765  reeanv 1778  rexeq1f 1784  cbvrexf 1797  cbvrex 1799  rexv 1821  rcla4e 1872  ceqsrexv 1889  reurex 1928  reu5 1929  reu2 1930  reu3 1931  reu6 1932  2reuswap 1937  reuss2 2275  reuun2 2278  reupick 2279  rabn0 2292  rab0 2293  r19.2z 2347  dfuni2 2505  eluni2 2507  elunirab 2514  iunconst 2572  dfiun2g 2586  dfiin2 2588  iunss 2591  ssiun 2592  iinss 2600  iunid 2603  iunn0 2607  iunxsn 2612  iunxun 2614  iununi 2616  intexrab 2732  onminex 3020  elxp2 3203  dmuni 3319  rnopab2 3354  dfima2 3405  dfima3 3406  elima2 3409  imasng 3424  rnuni 3459  rninxp 3482  imaco 3501  zfrep6 3614  fv2 3720  fnrnfv 3759  dffo4 3820  dffo5 3821  abrexexlem1 3858  imaiun 3864  abexssex 3872  abexex 3873  isomin 3899  iinon 3910  tfrlem8 3918  rdglim2 3949  oarec 4196  elqs 4290  qsexg 4294  snec 4296  mapsn 4345  mapsnen 4429  pssnn 4534  unblem2 4541  unfilem1 4548  zfregcl 4595  axinf2 4624  zfinf 4626  r1pwcl 4687  rankuni 4698  scott0 4717  cp 4722  bnd2 4724  aceq1 4729  aceq5lem2 4736  aceq5lem3 4737  aceq6b 4742  ac6lem 4754  kmlem3 4767  kmlem6 4770  kmlem8 4772  kmlem14 4778  zorn2lem6 4793  cfub 4908  ltexpi 5029  prnmax 5099  genpcl 5111  1pr 5117  ltexprlem5 5146  reclem2pr 5157  suplem1pr 5161  axrnegex 5283  axrrecex 5284  pre-axsup 5291  renegcl 5416  0re 5440  ssxr 5540  redivcl 5798  sup2 6051  infm3 6054  infmsup 6068  nnunb 6070  xrsupsslem 6076  xrinfmsslem 6077  supxrre 6083  2rexuz 6446  nnwof 6459  nnwos 6460  creur 6742  creui 6743  replimt 6761  infcvglem1 7221  ivthlem3 7283  ivthlem7 7287  infxpidmlem9 7560  infxpidmlem10 7561  isbasis2g 7612  tgval2t 7617  tgval3t 7625  tgss3t 7638  basgent 7640  cncfmet 7905  bcthlem8 8006  bcthlem14 8012  ubthlem6 8534  grothinf 8781  grothprim 8783  chsscm 9112  chcmh 9113  shne0 9371  nmcopexlem1 9951  nmcfnexlem1 9980  cnlnssadj 10013  faimpex 10438  abfi 10451  abfiOLD 10452  ficli 10472  ficliOLD 10473  hmeogrp 10538

Copyright terms: Public domain