Definition df-rex 1647

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 1643	. 2 wff ∃x ∈ A φ
5	2	cv 953	. . . . 5 class x
6	5, 3	wcel 956	. . . 4 wff x ∈ A
7	6, 1	wa 223	. . 3 wff (x ∈ A ⋀ φ)
8	7, 2	wex 978	. 2 wff ∃x(x ∈ A ⋀ φ)
9	4, 8	wb 146	1 wff (∃x ∈ A φ ↔ ∃x(x ∈ A ⋀ φ))

This definition is referenced by:  ralnex 1650  rexnal 1651  rexbida 1655  rexbidv2 1663  rexbii2 1669  risset 1682  hbrex 1685  hbre1 1686  r2ex 1688  rexex 1690  ra4e 1692  r19.22 1728  r19.22i2 1730  r19.22dv2 1733  r19.23v 1738  r19.23ai 1739  r19.23ad 1742  r19.29 1753  r19.41v 1760  r19.43 1762  reeanv 1775  rexeq1f 1781  cbvrex 1795  rexv 1817  rcla4e 1868  ceqsrexv 1885  reurex 1924  reu5 1925  reu2 1926  reu3 1927  reu6 1928  2reuswap 1933  reuss2 2271  reuun2 2274  reupick 2275  rabn0 2288  rab0 2289  r19.2z 2343  dfuni2 2500  eluni2 2502  elunirab 2509  iunconst 2567  dfiun2g 2581  dfiin2 2583  iunss 2586  ssiun 2587  iinss 2595  iunid 2598  iunn0 2602  iunxsn 2607  iunxun 2609  iununi 2611  intexrab 2727  onminex 3015  nnsuc 3143  elxp2 3198  dmuni 3314  rnopab2 3348  dfima2 3397  dfima3 3398  elima2 3401  imasng 3416  rnuni 3451  rninxp 3474  imaco 3493  zfrep6 3606  fv2 3711  fnrnfv 3750  dffo4 3811  dffo5 3812  abrexexlem1 3849  imaiun 3855  abexssex 3863  abexex 3864  isomin 3890  iinon 3901  tfrlem8 3909  rdglim2 3940  oarec 4186  elqs 4280  qsexg 4284  snec 4286  mapsn 4335  mapsnen 4416  pssnn 4519  ssnn 4520  unblem2 4524  unfilem1 4530  zfregcl 4575  axinf2 4604  zfinf 4606  r1pwcl 4667  rankuni 4678  scott0 4697  cp 4702  bnd2 4704  aceq1 4709  aceq5lem2 4716  aceq5lem3 4717  aceq6b 4722  ac6lem 4734  kmlem3 4747  kmlem6 4750  kmlem8 4752  kmlem14 4758  zorn2lem6 4773  zorn2lem7 4774  alephval3 4883  cfub 4888  ltexpi 5009  prnmax 5079  genpcl 5091  1pr 5097  ltexprlem5 5126  reclem2pr 5137  suplem1pr 5141  axrnegex 5263  axrrecex 5264  pre-axsup 5271  renegcl 5396  0re 5420  ssxr 5521  redivcl 5762  sup2 6006  infm3 6009  infmsup 6023  nnunb 6025  xrsupsslem 6031  xrinfmsslem 6032  supxrre 6038  2rexuz 6386  nnwof 6399  nnwos 6400  creur 6681  creui 6682  replimt 6700  infcvglem1 7164  ivthlem3 7226  ivthlem7 7230  ivthlem7OLD 7239  infxpidmlem9 7511  infxpidmlem10 7512  isbasis2g 7562  tgval2t 7567  tgval3t 7575  tgss3t 7588  basgent 7590  cncfmet 7857  bcthlem8 7956  bcthlem14 7962  ubthlem6 8478  grothinf 8720  grothprim 8722  chsscm 9051  chcmh 9052  shless 9285  shne0 9309  nmcopexlem1 9889  nmcfnexlem1 9918  cnlnssadj 9951  cbvrexf 10374  faimpex 10375  abfi 10385  ficli 10404  hmeogrp 10461

Copyright terms: Public domain