Definition df-rex 2481

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

This definition is referenced by:  ralnex  2485  rexnalim  2486  dfrex2dc  2488  rexbida  2492  rexbidv2  2500  rexbid2  2502  rexbii2  2508  r2exf  2515  risset  2525  nfrexdxy  2531  nfrexdya  2533  nfre1  2540  rexex  2543  rspe  2546  rsp2e  2548  rexim  2591  reximi2  2593  reximdv2  2596  r19.23t  2604  r19.41  2652  r19.43  2655  reean  2666  rexeqf  2690  reu5  2714  rmo5  2717  cbvrexfw  2720  cbvrexf  2722  cbvrexvw  2734  cbvrexdva2  2737  rexv  2781  2gencl  2796  3gencl  2797  rspce  2863  rspcimedv  2870  ceqsrexv  2894  rexab  2926  rexab2  2930  rexrab2  2931  morex  2948  reu2  2952  reu6  2953  reu3  2954  2reuswapdc  2968  2rmorex  2970  cbvrexcsf  3148  ssrexf  3245  rexun  3343  reuss2  3443  reuun2  3446  reupick  3447  reupick3  3448  reximdva0m  3466  rabn0r  3477  rabn0m  3478  r19.2m  3537  r19.2mOLD  3538  r19.9rmv  3542  rexm  3550  rexsns  3661  exsnrex  3664  dfuni2  3841  eluni2  3843  elunirab  3852  iuncom4  3923  iunxiun  3998  intexrabim  4186  bnd2  4206  rexxfrd  4498  elxp2  4681  opeliunxp  4718  xpiundi  4721  xpiundir  4722  rexiunxp  4808  dmuni  4876  rnmpt  4914  elrnmpt1  4917  elres  4982  dfima2  5011  dfima3  5012  elima2  5015  dfco2a  5170  imaco  5175  imadiflem  5337  imadif  5338  imainlem  5339  imain  5340  funimaexglem  5341  fvelrnb  5608  rexrnmpt  5705  dffo4  5710  dffo5  5711  abrexco  5806  opabex3d  6178  opabex3  6179  abexssex  6182  abexex  6183  ecexr  6597  mapsn  6749  mapsnen  6870  fimax2gtri  6962  ctssdccl  7177  ltexnqq  7475  subhalfnqq  7481  ltbtwnnq  7483  nqnq0  7508  prnmaxl  7555  prnminu  7556  prarloc  7570  genpdflem  7574  genpassl  7591  genpassu  7592  nqprm  7609  nqprl  7618  nqpru  7619  ltsopr  7663  ltexprlemm  7667  ltexprlemloc  7674  suplocexprlemrl  7784  suplocexprlemloc  7788  axprecex  7947  axpre-ltirr  7949  sup3exmid  8984  2rexuz  9656  ioom  10350  nnwosdc  12206  4sqlemafi  12564  inffinp1  12646  omctfn  12660  nninfdclemp1  12667  ptex  12935  fngsum  13031  igsumvalx  13032  isbasis2g  14281  tgval2  14287  ntreq0  14368  bdcuni  15522  bj-axun2  15561