Definition df-rex 2360

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 2356	. 2 wff E.x e. A ph
5	2	cv 1585	. . . . 5 class x
6	5, 3	wcel 1588	. . . 4 wff x e. A
7	6, 1	wa 337	. . 3 wff (x e. A /\ ph)
8	7, 2	wex 1615	. 2 wff E.x(x e. A /\ ph)
9	4, 8	wb 219	1 wff (E.x e. A ph <-> E.x(x e. A /\ ph))

This definition is referenced by:  ralnex 2363  rexnal 2364  rexbida 2368  rexbidv2 2376  rexbii2 2382  risset 2395  hbrex 2400  hbre1 2401  r2ex 2403  rexex 2405  ra4e 2407  reximi2 2447  reximdv2 2450  r19.23t 2455  r19.23 2456  r19.41 2482  reean 2492  rexeqf 2509  cbvrexf 2523  rexv 2553  rcla4e 2615  ceqsrexv 2634  morex 2682  reurex 2686  reu5 2687  reu2 2688  reu6 2689  reu3 2690  2reuswap 2695  cbvrexcsf 2821  rexun 2996  reuss2 3077  reuun2 3080  reupick 3081  reximdva0 3093  rabn0 3100  r19.2z 3158  r19.2zb 3159  rexsng 3265  dfuni2 3368  eluni2 3370  elunirab 3379  iunxsn 3497  iunxun 3499  iununi 3501  intexrab 3635  reusv2lem4 3970  reusv5OLD 3976  eusvobj1 3980  onminex 4031  elxp2 4152  dmuni 4291  rnopab2 4324  elres 4368  dfima2 4385  dfima3 4386  elima2 4389  rnuni 4436  dfco2a 4496  imaco 4501  iunfopab 4639  zfrep6 4641  fnrnfv 4804  dffo4 4883  dffo5 4884  abrexexlem1 4927  opabex3 4933  imaiun 4935  abexssex 4943  abexex 4944  isomin 4972  frxp 5210  iinon 5252  onopriun 5255  tfrlem8 5290  rdglim2 5321  oarec 5407  qsexg 5513  snec 5516  mapsn 5565  mapsnen 5650  mapsnenOLD 5651  fineqvlem 5829  pssnn 5834  unblem2 5853  unfilem1 5860  zfregcl 5930  axinf2 5963  zfinf2 5965  r1pwcl 6034  rankuni 6045  onfrALTlem5 6076  onfrALTlem2 6080  onfrALTlem1 6082  scott0 6086  cp 6091  bnd2 6093  aceq1 6183  aceq5lem2 6190  aceq5lem3 6191  aceq6b 6196  cfub 6268  cfval2 6280  cflim3 6282  ac6lem 6324  kmlem3 6339  kmlem6 6342  kmlem8 6344  kmlem14 6350  zorn2lem6 6366  ltexpi 6547  prnmax 6617  genpcl 6629  1pr 6635  ltexprlem5 6664  reclem2pr 6675  suplem1pr 6679  axrnegex 6799  axrrecex 6800  pre-axsup 6807  redivcli 7307  sup2 7600  infm3 7603  infmsup 7617  nnunb 7619  xrsupsslem 7625  xrinfmsslem 7626  supxrre 7632  2rexuz 7962  nnwof 7975  nnwos 7976  creur 8376  creui 8377  replim 8395  infcvglem1OLD 8880  ivthlem3 8943  ivthlem7 8947  infxpidmlem9OLD 9223  infxpidmlem10OLD 9224  maxprmfct 9383  isbasis2g 9732  tgval2 9738  tgval3 9746  tgss3 9759  basgen 9761  cncfmet 10049  bcthlem8 10150  bcthlem14 10156  ubthlem6 10746  grothomex 11007  grothprim 11012  abfi 11050  isfbas2 11101  fbssint 11117  elfg 11122  fgfil 11128  chsscmi 11579  chcmhi 11580  shne0i 11838  nmcopexlem1 12420  nmcfnexlem1 12449  cnlnssadj 12482  bnj168 13273  bnj214 13282  bnj512 13292  bnj537 13305  bnj542 13308  bnj901 13589  bnj903 13590  bnj912 13593  bnj957 13623  bnj1098 13688  bnj1144 13712  bnj1146 13714  bnj1158 13721  bnj1160 13723  bnj1184 13737  bnj1185 13738  bnj1196 13743  bnj1267 13797  bnj1306 13820  bnj1310 13821  bnj1330 13832  bnj1396 13881  bnj1402 13883  bnj1481 13929  bnj1492 13932  bnj1506 13937  bnj70 13976  bnj849 14089  bnj916 14103  bnj983 14128  bnj984 14129  bnj1083 14179  bnj1498 14333  elresOLD 14454  coep 14461  coepr 14462  dffr5 14463  dfpo2 14465  dfon2lem8 14490  frxpOLD 14604  tfrALTlem 14629  axfelem18 14716  fates 14992  ra42e 15001  ficli 15063  cbicplem 15247  dstr 15255  iscst4 15261  domncnt 15363  ranncnt 15364  apnei 15623  hmeogrp 15649  sbtpsines 15667  stoig2b 15668  settrcon 16057  tmpts 16067  opncldf1 16226  compfipin0 16260  alexsublem4 16264  reconnlem5 16274  is1stc3 16293  isfne2 16305  isfne3 16306  neibastop2lem3 16345  neibastop2 16347  fnejoin2 16355  neifg 16383  rexunOLD 16480  morexOLD 16486  opabex3OLD 16525  abrexdom 16563  firnfi3 16567  sstotbnd 16760  heiborlem13 16791  heiborlem17 16795  heiborlem37 16815  rrncms 16843  prtlem5 17069  n0el 17072  erdisj3 17090  prtlem16 17096  prtlem17 17102  prtlem18 17103  prter2 17109  prter3 17110  cbvrexcsfOLD 17236  rexbidar 17247  onfrALTlem5VD 17543  onfrALTlem2VD 17547  onfrALTlem1VD 17548  hl1at 17785  atex 17801  islpln5 17966  islvol5 18011  pmapglb 18202  pmapglb2 18203  pmapglb2x 18204  elpaddn0 18232  pmapjat1 18285  polval2 18323  osumcllem11 18379  pexmidlem8 18390

Copyright terms: Public domain