Definition df-rex 2110

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 2106	. 2 wff E.x e. A ph
5	2	cv 1297	. . . . 5 class x
6	5, 3	wcel 1300	. . . 4 wff x e. A
7	6, 1	wa 240	. . 3 wff (x e. A /\ ph)
8	7, 2	wex 1326	. 2 wff E.x(x e. A /\ ph)
9	4, 8	wb 163	1 wff (E.x e. A ph <-> E.x(x e. A /\ ph))

This definition is referenced by:  ralnex 2113  rexnal 2114  rexbida 2118  rexbidv2 2126  rexbii2 2132  risset 2145  hbrex 2149  hbre1 2150  r2ex 2152  rexex 2154  ra4e 2156  reximOLD 2195  reximi2 2197  reximdv2 2200  r19.23 2206  r19.23OLD 2207  r19.23aiOLD 2210  r19.23adOLD 2214  r19.29OLD 2228  r19.41 2235  r19.43OLD 2239  reean 2247  reeanOLD 2248  rexeqf 2264  cbvrexf 2277  rexv 2306  rcla4e 2375  ceqsrexv 2394  reurex 2440  reu5 2441  reu2 2442  reu6 2443  reu3 2444  2reuswap 2449  rexun 2783  reuss2 2870  reuun2 2873  reupick 2874  reximdva0 2886  rabn0 2893  rab0OLD 2895  r19.2z 2958  r19.2zb 2959  rexsng 3072  dfuni2 3179  eluni2 3181  elunirab 3190  iunconstOLD 3263  dfiun2gOLD 3284  dfiin2OLD 3288  iunssOLD 3292  ssiunOLD 3294  iinssOLD 3305  iunn0OLD 3316  iunxsn 3327  iunxun 3329  iununi 3331  iununiOLD 3332  intexrab 3468  eufromeq4 3831  euobj1 3834  onminex 3888  elxp2 4019  dmuni 4166  rnopab2 4202  dfima2 4265  dfima2OLD 4266  dfima3 4267  dfima3OLD 4268  elima2 4271  rnuni 4327  rninxpOLD 4356  dfco2a 4394  imaco 4403  iunfopab 4542  iunfopabOLD 4543  zfrep6 4545  fv2OLD 4677  fnrnfv 4718  dffo4 4793  dffo5 4794  abrexexlem1 4834  imaiun 4840  abexssex 4848  abexex 4849  isomin 4876  iinon 5115  onopriun 5118  tfrlem8 5126  rdglim2 5157  oarec 5244  qsexg 5352  snec 5355  mapsn 5404  mapsnen 5488  pssnn 5628  unblem2 5634  unfilem1 5641  zfregcl 5697  axinf2 5730  zfinf2 5732  r1pwcl 5798  rankuni 5809  scott0 5847  cp 5852  bnd2 5854  aceq1 5891  aceq5lem2 5898  aceq5lem3 5899  aceq6b 5904  ac6lem 5916  kmlem3 5929  kmlem6 5932  kmlem8 5934  kmlem14 5940  zorn2lem6 5955  cfub 6056  ltexpi 6181  prnmax 6251  genpcl 6263  1pr 6269  ltexprlem5 6298  reclem2pr 6309  suplem1pr 6313  axrnegex 6436  axrrecex 6437  pre-axsup 6444  renegcliOLD 6577  0re 6603  ssxrOLD 6715  redivcli 6976  sup2 7260  infm3 7263  infmsup 7277  nnunb 7279  xrsupsslem 7285  xrinfmsslem 7286  supxrre 7292  2rexuz 7615  nnwof 7628  nnwos 7629  creur 7992  creui 7993  replim 8011  infcvglem1 8482  ivthlem3 8545  ivthlem7 8549  infxpidmlem9 8829  infxpidmlem10 8830  isbasis2g 8881  tgval2 8887  tgval3 8895  tgss3 8908  basgen 8910  cncfmet 9183  bcthlem8 9284  bcthlem14 9290  ubthlem6 9877  grothomex 10136  grothprim 10141  abfi 10215  isfbas2 10263  fbssint 10279  elfg 10284  fgfil 10290  chsscmi 10745  chcmhi 10746  shne0i 11004  nmcopexlem1 11588  nmcfnexlem1 11617  cnlnssadj 11650  bnj10OLD 12375  bnj11OLD 12377  bnj14OLD 12382  bnj32OLD 12399  bnj162OLD 12488  bnj168 12496  bnj214 12508  bnj512 12519  bnj537 12533  bnj542 12536  bnj901 12818  bnj903 12819  bnj912 12822  bnj957 12852  bnj1098 12917  bnj1144 12941  bnj1146 12943  bnj1158 12950  bnj1160 12952  bnj1184 12966  bnj1185 12967  bnj1196 12972  bnj1267 13026  bnj1306 13049  bnj1310 13050  bnj1330 13061  bnj1396 13110  bnj1402 13112  bnj1481 13158  bnj1492 13161  bnj1506 13166  bnj70 13205  bnj849 13318  bnj916 13332  bnj983 13357  bnj984 13358  bnj1083 13408  bnj1498 13562  elres 13824  dffr5 13831  dfon2lem8 13856  frxp 13951  tfrALTlem 13976  axfelem11 14041  axfelem15 14045  fates 14292  ficli 14353  cbicplem 14508  dstr 14516  iscst4 14522  domncnt 14624  ranncnt 14625  hmeogrp 14892  sbtpsines 14905  stoig2b 14906  settrcon 15247  tmpts 15257  opncldf1 15402  compfipin0 15436  alexsublem4 15440  reconnlem5 15450  is1stc3 15469  isfne2 15481  isfne3 15482  neibastop2lem3 15521  neibastop2 15523  fnejoin2 15531  neifg 15559  rexunOLD 15656  morex 15662  opabex3 15701  abrexdom 15739  firnfi3 15743  sstotbnd 15936  heiborlem13 15967  heiborlem17 15971  heiborlem37 15991  rrncms 16019  prtlem5 16245  n0el 16248  erdisj3 16266  prtlem16 16272  prtlem17 16278  prtlem18 16279  prter2 16285  prter3 16286  cbvrexcsf 16412  rexbidar 16423  hl1atom 17040  pmapglb 17252  pmapglb2 17253  pmapglb2x 17254  elpaddn0 17261  pmapjat 17314  polval2 17319  osumcllem11 17374  pexmidlem8 17385

Copyright terms: Public domain