Definition df-rex 1696

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

Assertion

Ref	Expression
df-rex	⊢ (∃x ∈ A φ ↔ ∃x(x ∈ A ⋀ φ))

Detailed syntax breakdown of Definition df-rex

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		vx	. . 3 set x
3		cA	. . 3 class A
4	1, 2, 3	wrex 1692	. 2 wff ∃x ∈ A φ
5	2	cv 991	. . . . 5 class x
6	5, 3	wcel 994	. . . 4 wff x ∈ A
7	6, 1	wa 221	. . 3 wff (x ∈ A ⋀ φ)
8	7, 2	wex 1016	. 2 wff ∃x(x ∈ A ⋀ φ)
9	4, 8	wb 144	1 wff (∃x ∈ A φ ↔ ∃x(x ∈ A ⋀ φ))

This definition is referenced by:  ralnex 1699  rexnal 1700  rexbida 1704  rexbidv2 1712  rexbii2 1718  risset 1731  hbrex 1734  hbre1 1735  r2ex 1737  rexex 1739  ra4e 1741  r19.22 1777  r19.22i2 1779  r19.22dv2 1782  r19.23v 1787  r19.23ai 1788  r19.23ad 1791  r19.29 1802  r19.41v 1809  r19.43 1811  reeanv 1824  rexeq1f 1830  cbvrexf 1843  cbvrex 1845  rexv 1867  rcla4e 1918  ceqsrexv 1935  reurex 1974  reu5 1975  reu2 1976  reu3 1977  reu6 1978  2reuswap 1983  reuss2 2327  reuun2 2330  reupick 2331  rabn0 2345  rab0 2346  r19.2z 2401  dfuni2 2571  eluni2 2573  elunirab 2580  iunconst 2640  dfiun2g 2654  dfiin2 2656  iunss 2659  ssiun 2660  iinss 2668  iunn0 2676  iunxsn 2682  iunxun 2684  iununi 2686  intexrab 2806  onminex 3164  elxp2 3284  dmuni 3410  rnopab2 3441  dfima2 3497  dfima3 3498  elima2 3501  imasng 3516  rnuni 3544  rninxp 3567  imaco 3604  iunfopab 3719  zfrep6 3721  fv2 3831  fnrnfv 3870  dffo4 3934  dffo5 3935  abrexexlem1 3972  imaiun 3978  abexssex 3986  abexex 3987  isomin 4013  iinon 4208  onopriun 4211  tfrlem8 4219  rdglim2 4250  oarec 4332  qsexg 4434  snec 4437  mapsn 4486  mapsnen 4570  pssnn 4681  unblem2 4687  unfilem1 4694  zfregcl 4738  axinf2 4769  zfinf2 4771  r1pwcl 4833  rankuni 4844  scott0 4863  cp 4868  bnd2 4870  aceq1 4875  aceq5lem2 4882  aceq5lem3 4883  aceq6b 4888  ac6lem 4900  kmlem3 4913  kmlem6 4916  kmlem8 4918  kmlem14 4924  zorn2lem6 4939  cfub 5058  ltexpi 5183  prnmax 5253  genpcl 5265  1pr 5271  ltexprlem5 5300  reclem2pr 5311  suplem1pr 5315  axrnegex 5437  axrrecex 5438  pre-axsup 5445  renegcli 5570  0re 5594  ssxr 5694  redivcli 5938  sup2 6219  infm3 6222  infmsup 6236  nnunb 6238  xrsupsslem 6244  xrinfmsslem 6245  supxrre 6251  2rexuz 6573  nnwof 6586  nnwos 6587  creur 6943  creui 6944  replim 6962  infcvglem1 7425  ivthlem3 7488  ivthlem7 7492  infxpidmlem9 7772  infxpidmlem10 7773  isbasis2g 7824  tgval2 7829  tgval3 7837  tgss3 7850  basgen 7852  cncfmet 8116  bcthlem8 8217  bcthlem14 8223  ubthlem6 8792  grothinf 9053  grothprim 9057  chsscmi 9388  chcmhi 9389  shne0i 9647  nmcopexlem1 10230  nmcfnexlem1 10259  cnlnssadj 10292  abfi 10737  ficli 10756  domncnt 10872  ranncnt 10873  hmeogrp 11044  sbtpsines 11062  r19.2zb 11393  opncldf1 11454  compfipin0 11493  alexsublem4 11499  reconnlem5 11511  is1stc3 11530  isfne2 11542  isfne3 11543  neibastop2lem3 11582  neibastop2 11584  fnejoin2 11592  isfbas2 11622  fbssint 11626  elfg 11633  fgfil 11638  neifg 11644  morex 11804  opabex3 11806  abrexdom 11826  firnfi3 11830  metsstop 11909  sstotbnd 11992  heiborlem13 12023  heiborlem17 12027  heiborlem37 12047  rrncms 12075

Copyright terms: Public domain