Definition df-rex 2478

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 2473	. 2 wff E. x e. A ph
5	2	cv 1363	. . . . 5 class x
6	5, 3	wcel 2164	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	wex 1503	. 2 wff E. x ( x e. A /\ ph )
9	4, 8	wb 105	1 wff ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )

This definition is referenced by:  ralnex  2482  rexnalim  2483  dfrex2dc  2485  rexbida  2489  rexbidv2  2497  rexbid2  2499  rexbii2  2505  r2exf  2512  risset  2522  nfrexdxy  2528  nfrexdya  2530  nfre1  2537  rexex  2540  rspe  2543  rsp2e  2545  rexim  2588  reximi2  2590  reximdv2  2593  r19.23t  2601  r19.41  2649  r19.43  2652  reean  2663  rexeqf  2687  reu5  2711  rmo5  2714  cbvrexfw  2717  cbvrexf  2719  cbvrexvw  2731  cbvrexdva2  2734  rexv  2778  2gencl  2793  3gencl  2794  rspce  2859  rspcimedv  2866  ceqsrexv  2890  rexab  2922  rexab2  2926  rexrab2  2927  morex  2944  reu2  2948  reu6  2949  reu3  2950  2reuswapdc  2964  2rmorex  2966  cbvrexcsf  3144  ssrexf  3241  rexun  3339  reuss2  3439  reuun2  3442  reupick  3443  reupick3  3444  reximdva0m  3462  rabn0r  3473  rabn0m  3474  r19.2m  3533  r19.2mOLD  3534  r19.9rmv  3538  rexm  3546  rexsns  3657  exsnrex  3660  dfuni2  3837  eluni2  3839  elunirab  3848  iuncom4  3919  iunxiun  3994  intexrabim  4182  bnd2  4202  rexxfrd  4492  elxp2  4675  opeliunxp  4712  xpiundi  4715  xpiundir  4716  rexiunxp  4800  dmuni  4868  rnmpt  4906  elrnmpt1  4909  elres  4974  dfima2  5003  dfima3  5004  elima2  5007  dfco2a  5162  imaco  5167  imadiflem  5329  imadif  5330  imainlem  5331  imain  5332  funimaexglem  5333  fvelrnb  5600  rexrnmpt  5697  dffo4  5702  dffo5  5703  abrexco  5798  opabex3d  6169  opabex3  6170  abexssex  6173  abexex  6174  ecexr  6587  mapsn  6739  mapsnen  6860  fimax2gtri  6952  ctssdccl  7164  ltexnqq  7462  subhalfnqq  7468  ltbtwnnq  7470  nqnq0  7495  prnmaxl  7542  prnminu  7543  prarloc  7557  genpdflem  7561  genpassl  7578  genpassu  7579  nqprm  7596  nqprl  7605  nqpru  7606  ltsopr  7650  ltexprlemm  7654  ltexprlemloc  7661  suplocexprlemrl  7771  suplocexprlemloc  7775  axprecex  7934  axpre-ltirr  7936  sup3exmid  8970  2rexuz  9641  ioom  10323  nnwosdc  12170  4sqlemafi  12527  inffinp1  12580  omctfn  12594  nninfdclemp1  12601  ptex  12869  fngsum  12965  igsumvalx  12966  isbasis2g  14194  tgval2  14200  ntreq0  14281  bdcuni  15346  bj-axun2  15385