Definition df-rex 2354

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	|- ( 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 setvar x
3		cA	. . 3 class A
4	1, 2, 3	wrex 2349	. 2 wff E. x e. A ph
5	2	cv 1283	. . . . 5 class x
6	5, 3	wcel 1433	. . . 4 wff x e. A
7	6, 1	wa 102	. . 3 wff ( x e. A /\ ph )
8	7, 2	wex 1421	. 2 wff E. x ( x e. A /\ ph )
9	4, 8	wb 103	1 wff ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )

This definition is referenced by:  ralnex  2358  rexnalim  2359  rexbida  2363  rexbidv2  2371  rexbii2  2377  r2exf  2384  risset  2394  nfrexdxy  2399  nfrexdya  2401  nfre1  2407  rexex  2410  rspe  2412  rsp2e  2414  rexim  2455  reximi2  2457  reximdv2  2460  r19.23t  2467  r19.41  2509  r19.43  2512  reean  2522  rexeqf  2546  reu5  2566  rmo5  2569  cbvrexf  2572  cbvrexdva2  2582  rexv  2617  2gencl  2632  3gencl  2633  rspce  2696  rspcimedv  2703  ceqsrexv  2725  rexab  2754  rexab2  2758  rexrab2  2759  morex  2776  reu2  2780  reu6  2781  reu3  2782  2reuswapdc  2794  2rmorex  2796  cbvrexcsf  2965  rexun  3152  reuss2  3244  reuun2  3247  reupick  3248  reupick3  3249  reximdva0m  3263  rabn0r  3271  rabn0m  3272  r19.2m  3329  r19.9rmv  3333  rexm  3340  rexsns  3432  exsnrex  3435  dfuni2  3603  eluni2  3605  elunirab  3614  iuncom4  3685  iunxiun  3757  intexrabim  3928  bnd2  3947  rexxfrd  4213  elxp2  4381  opeliunxp  4413  xpiundi  4416  xpiundir  4417  rexiunxp  4496  dmuni  4563  rnmpt  4600  elrnmpt1  4603  elres  4664  dfima2  4690  dfima3  4691  elima2  4694  dfco2a  4841  imaco  4846  imadiflem  4998  imadif  4999  imainlem  5000  imain  5001  funimaexglem  5002  fvelrnb  5242  rexrnmpt  5331  dffo4  5336  dffo5  5337  abrexco  5419  opabex3d  5768  opabex3  5769  abexssex  5772  abexex  5773  ecexr  6134  ltexnqq  6598  subhalfnqq  6604  ltbtwnnq  6606  nqnq0  6631  prnmaxl  6678  prnminu  6679  prarloc  6693  genpdflem  6697  genpassl  6714  genpassu  6715  nqprm  6732  nqprl  6741  nqpru  6742  ltsopr  6786  ltexprlemm  6790  ltexprlemloc  6797  axprecex  7046  axpre-ltirr  7048  2rexuz  8670  ioom  9269  bdcuni  10667  bj-axun2  10706