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  5899  opabex3d  6282  opabex3  6283  abexssex  6286  abexex  6287  ecexr  6706  mapsn  6858  mapsnen  6985  fimax2gtri  7090  ctssdccl  7309  ltexnqq  7627  subhalfnqq  7633  ltbtwnnq  7635  nqnq0  7660  prnmaxl  7707  prnminu  7708  prarloc  7722  genpdflem  7726  genpassl  7743  genpassu  7744  nqprm  7761  nqprl  7770  nqpru  7771  ltsopr  7815  ltexprlemm  7819  ltexprlemloc  7826  suplocexprlemrl  7936  suplocexprlemloc  7940  axprecex  8099  axpre-ltirr  8101  sup3exmid  9136  2rexuz  9815  ioom  10519  nnwosdc  12609  4sqlemafi  12967  inffinp1  13049  omctfn  13063  nninfdclemp1  13070  ptex  13346  fngsum  13470  igsumvalx  13471  isbasis2g  14768  tgval2  14774  ntreq0  14855  bdcuni  16471  bj-axun2  16510