HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Definition df-rex 1642
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
StepHypRef Expression
1 wph . . 3 wff ph
2 vx . . 3 set x
3 cA . . 3 class A
41, 2, 3wrex 1638 . 2 wff E.x e. A ph
52cv 952 . . . . 5 class x
65, 3wcel 955 . . . 4 wff x e. A
76, 1wa 223 . . 3 wff (x e. A /\ ph)
87, 2wex 977 . 2 wff E.x(x e. A /\ ph)
94, 8wb 146 1 wff (E.x e. A ph <-> E.x(x e. A /\ ph))
Colors of variables: wff set class
This definition is referenced by:  ralnex 1645  rexnal 1646  rexbida 1650  rexbidv2 1658  rexbii2 1664  risset 1677  hbrex 1680  hbre1 1681  r2ex 1683  rexex 1685  ra4e 1687  r19.22 1723  r19.22i2 1725  r19.22dv2 1728  r19.23v 1733  r19.23ai 1734  r19.23ad 1737  r19.29 1748  r19.41v 1755  r19.43 1757  reeanv 1770  rexeq1f 1776  cbvrex 1790  rexv 1812  rcla4e 1863  ceqsrexv 1880  reurex 1918  reu5 1919  reu2 1920  reu3 1921  reu6 1922  2reuswap 1927  reuss2 2265  reuun2 2268  reupick 2269  rabn0 2282  rab0 2283  r19.2z 2337  dfuni2 2495  eluni2 2497  elunirab 2504  iunconst 2562  dfiun2g 2576  dfiin2 2578  iunss 2581  ssiun 2582  iinss 2590  iunid 2593  iunn0 2597  iunxsn 2602  iunxun 2604  iununi 2606  intexrab 2722  onminex 3010  nnsuc 3138  elxp2 3193  dmuni 3308  rnopab2 3340  dfima2 3389  dfima3 3390  elima2 3393  imasng 3408  rnuni 3445  rninxp 3468  imaco 3487  zfrep6 3600  fv2 3705  fnrnfv 3744  dffo4 3805  dffo5 3806  abrexexlem1 3843  imaiun 3849  abexssex 3857  abexex 3858  isomin 3884  iinon 3895  tfrlem8 3903  rdglim2 3934  oarec 4180  elqs 4274  qsexg 4278  snec 4280  mapsn 4329  mapsnen 4410  pssnn 4513  ssnn 4514  unblem2 4518  unfilem1 4524  zfregcl 4567  axinf2 4596  zfinf 4598  r1pwcl 4659  rankuni 4670  scott0 4689  cp 4694  bnd2 4696  aceq1 4701  aceq5lem2 4708  aceq5lem3 4709  aceq6b 4714  ac6lem 4726  kmlem3 4739  kmlem6 4742  kmlem8 4744  kmlem14 4750  zorn2lem6 4765  zorn2lem7 4766  alephval3 4875  cfub 4880  ltexpi 5001  prnmax 5071  genpcl 5083  1pr 5089  ltexprlem5 5118  reclem2pr 5129  suplem1pr 5133  axrnegex 5255  axrrecex 5256  pre-axsup 5263  renegcl 5388  0re 5412  ssxr 5513  redivcl 5754  sup2 5998  infm3 6001  infmsup 6015  nnunb 6017  xrsupsslem 6023  xrinfmsslem 6024  supxrre 6030  2rexuz 6378  nnwof 6391  nnwos 6392  creur 6673  creui 6674  replimt 6692  infcvglem1 7156  ivthlem3 7218  ivthlem7 7222  ivthlem7OLD 7231  infxpidmlem9 7503  infxpidmlem10 7504  isbasis2g 7554  tgval2t 7559  tgval3t 7567  tgss3t 7580  basgent 7582  cncfmet 7844  bcthlem8 7940  bcthlem14 7946  ubthlem6 8465  grothinf 8720  grothprim 8722  chsscm 9033  chcmh 9034  shless 9262  shne0 9286  nmcopexlem1 9866  nmcfnexlem1 9895  cnlnssadj 9928  cbvrexf 10338  faimpex 10339  abfi 10349  ficli 10368  hmeogrp 10425
Copyright terms: Public domain