Definition df-rex 2516

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 2511	. 2 wff ∃𝑥 ∈ 𝐴 𝜑
5	2	cv 1396	. . . . 5 class 𝑥
6	5, 3	wcel 2202	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 104	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wex 1540	. 2 wff ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 105	1 wff (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  ralnex  2520  rexnalim  2521  dfrex2dc  2523  rexbida  2527  rexbidv2  2535  rexbid2  2537  rexbii2  2543  r2exf  2550  risset  2560  nfrexdxy  2566  nfrexdya  2568  nfre1  2575  rexex  2578  rspe  2581  rsp2e  2583  rexim  2626  reximi2  2628  reximdv2  2631  r19.23t  2640  r19.41  2688  r19.43  2691  reean  2702  rexeqf  2727  reu5  2751  rmo5  2754  cbvrexfw  2757  cbvrexf  2759  cbvrexvw  2772  cbvrexdva2  2775  rexv  2821  2gencl  2836  3gencl  2837  rspce  2905  rspcimedv  2912  ceqsrexv  2936  rexab  2968  rexab2  2972  rexrab2  2973  morex  2990  reu2  2994  reu6  2995  reu3  2996  2reuswapdc  3010  2rmorex  3012  cbvrexcsf  3191  ssrexf  3289  rexun  3387  reuss2  3487  reuun2  3490  reupick  3491  reupick3  3492  reximdva0m  3510  rabn0r  3521  rabn0m  3522  r19.2m  3581  r19.2mOLD  3582  r19.9rmv  3586  rexm  3594  rexsns  3708  exsnrex  3711  dfuni2  3895  eluni2  3897  elunirab  3906  iuncom4  3977  iunxiun  4052  intexrabim  4243  bnd2  4263  rexxfrd  4560  elxp2  4743  opeliunxp  4781  xpiundi  4784  xpiundir  4785  rexiunxp  4872  ssrelrn  4922  dmuni  4941  rnmpt  4980  elrnmpt1  4983  elres  5049  dfima2  5078  dfima3  5079  elima2  5082  dfco2a  5237  imaco  5242  imadiflem  5409  imadif  5410  imainlem  5411  imain  5412  funimaexglem  5413  fvelrnb  5693  rexrnmpt  5790  dffo4  5795  dffo5  5796  abrexco  5900  opabex3d  6283  opabex3  6284  abexssex  6287  abexex  6288  ecexr  6707  mapsn  6859  mapsnen  6986  fimax2gtri  7091  ctssdccl  7310  ltexnqq  7628  subhalfnqq  7634  ltbtwnnq  7636  nqnq0  7661  prnmaxl  7708  prnminu  7709  prarloc  7723  genpdflem  7727  genpassl  7744  genpassu  7745  nqprm  7762  nqprl  7771  nqpru  7772  ltsopr  7816  ltexprlemm  7820  ltexprlemloc  7827  suplocexprlemrl  7937  suplocexprlemloc  7941  axprecex  8100  axpre-ltirr  8102  sup3exmid  9137  2rexuz  9816  ioom  10520  nnwosdc  12611  4sqlemafi  12969  inffinp1  13051  omctfn  13065  nninfdclemp1  13072  ptex  13348  fngsum  13472  igsumvalx  13473  isbasis2g  14771  tgval2  14777  ntreq0  14858  bdcuni  16474  bj-axun2  16513