Definition df-rex 2514

Description: Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22. (Contributed by NM, 30-Aug-1993.)

Assertion

Ref	Expression
df-rex	⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

Detailed syntax breakdown of Definition df-rex

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		cA	. . 3 class 𝐴
4	1, 2, 3	wrex 2509	. 2 wff ∃𝑥 ∈ 𝐴 𝜑
5	2	cv 1394	. . . . 5 class 𝑥
6	5, 3	wcel 2200	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 104	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wex 1538	. 2 wff ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 105	1 wff (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  ralnex  2518  rexnalim  2519  dfrex2dc  2521  rexbida  2525  rexbidv2  2533  rexbid2  2535  rexbii2  2541  r2exf  2548  risset  2558  nfrexdxy  2564  nfrexdya  2566  nfre1  2573  rexex  2576  rspe  2579  rsp2e  2581  rexim  2624  reximi2  2626  reximdv2  2629  r19.23t  2638  r19.41  2686  r19.43  2689  reean  2700  rexeqf  2725  reu5  2749  rmo5  2752  cbvrexfw  2755  cbvrexf  2757  cbvrexvw  2770  cbvrexdva2  2773  rexv  2818  2gencl  2833  3gencl  2834  rspce  2902  rspcimedv  2909  ceqsrexv  2933  rexab  2965  rexab2  2969  rexrab2  2970  morex  2987  reu2  2991  reu6  2992  reu3  2993  2reuswapdc  3007  2rmorex  3009  cbvrexcsf  3188  ssrexf  3286  rexun  3384  reuss2  3484  reuun2  3487  reupick  3488  reupick3  3489  reximdva0m  3507  rabn0r  3518  rabn0m  3519  r19.2m  3578  r19.2mOLD  3579  r19.9rmv  3583  rexm  3591  rexsns  3705  exsnrex  3708  dfuni2  3890  eluni2  3892  elunirab  3901  iuncom4  3972  iunxiun  4047  intexrabim  4237  bnd2  4257  rexxfrd  4554  elxp2  4737  opeliunxp  4774  xpiundi  4777  xpiundir  4778  rexiunxp  4864  ssrelrn  4914  dmuni  4933  rnmpt  4972  elrnmpt1  4975  elres  5041  dfima2  5070  dfima3  5071  elima2  5074  dfco2a  5229  imaco  5234  imadiflem  5400  imadif  5401  imainlem  5402  imain  5403  funimaexglem  5404  fvelrnb  5683  rexrnmpt  5780  dffo4  5785  dffo5  5786  abrexco  5889  opabex3d  6272  opabex3  6273  abexssex  6276  abexex  6277  ecexr  6693  mapsn  6845  mapsnen  6972  fimax2gtri  7071  ctssdccl  7286  ltexnqq  7603  subhalfnqq  7609  ltbtwnnq  7611  nqnq0  7636  prnmaxl  7683  prnminu  7684  prarloc  7698  genpdflem  7702  genpassl  7719  genpassu  7720  nqprm  7737  nqprl  7746  nqpru  7747  ltsopr  7791  ltexprlemm  7795  ltexprlemloc  7802  suplocexprlemrl  7912  suplocexprlemloc  7916  axprecex  8075  axpre-ltirr  8077  sup3exmid  9112  2rexuz  9785  ioom  10488  nnwosdc  12568  4sqlemafi  12926  inffinp1  13008  omctfn  13022  nninfdclemp1  13029  ptex  13305  fngsum  13429  igsumvalx  13430  isbasis2g  14727  tgval2  14733  ntreq0  14814  bdcuni  16263  bj-axun2  16302