Definition df-rex 2514

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

This definition is referenced by:  ralnex  2518  rexnalim  2519  dfrex2dc  2521  rexbida  2525  rexbidv2  2533  rexbid2  2535  rexbii2  2541  r2exf  2548  risset  2558  nfrexdxy  2564  nfrexdya  2566  nfre1  2573  rexex  2576  rspe  2579  rsp2e  2581  rexim  2624  reximi2  2626  reximdv2  2629  r19.23t  2638  r19.41  2686  r19.43  2689  reean  2700  rexeqf  2725  reu5  2749  rmo5  2752  cbvrexfw  2755  cbvrexf  2757  cbvrexvw  2770  cbvrexdva2  2773  rexv  2819  2gencl  2834  3gencl  2835  rspce  2903  rspcimedv  2910  ceqsrexv  2934  rexab  2966  rexab2  2970  rexrab2  2971  morex  2988  reu2  2992  reu6  2993  reu3  2994  2reuswapdc  3008  2rmorex  3010  cbvrexcsf  3189  ssrexf  3287  rexun  3385  reuss2  3485  reuun2  3488  reupick  3489  reupick3  3490  reximdva0m  3508  rabn0r  3519  rabn0m  3520  r19.2m  3579  r19.2mOLD  3580  r19.9rmv  3584  rexm  3592  rexsns  3706  exsnrex  3709  dfuni2  3891  eluni2  3893  elunirab  3902  iuncom4  3973  iunxiun  4048  intexrabim  4239  bnd2  4259  rexxfrd  4556  elxp2  4739  opeliunxp  4777  xpiundi  4780  xpiundir  4781  rexiunxp  4868  ssrelrn  4918  dmuni  4937  rnmpt  4976  elrnmpt1  4979  elres  5045  dfima2  5074  dfima3  5075  elima2  5078  dfco2a  5233  imaco  5238  imadiflem  5404  imadif  5405  imainlem  5406  imain  5407  funimaexglem  5408  fvelrnb  5687  rexrnmpt  5784  dffo4  5789  dffo5  5790  abrexco  5893  opabex3d  6276  opabex3  6277  abexssex  6280  abexex  6281  ecexr  6700  mapsn  6852  mapsnen  6979  fimax2gtri  7082  ctssdccl  7299  ltexnqq  7616  subhalfnqq  7622  ltbtwnnq  7624  nqnq0  7649  prnmaxl  7696  prnminu  7697  prarloc  7711  genpdflem  7715  genpassl  7732  genpassu  7733  nqprm  7750  nqprl  7759  nqpru  7760  ltsopr  7804  ltexprlemm  7808  ltexprlemloc  7815  suplocexprlemrl  7925  suplocexprlemloc  7929  axprecex  8088  axpre-ltirr  8090  sup3exmid  9125  2rexuz  9804  ioom  10508  nnwosdc  12597  4sqlemafi  12955  inffinp1  13037  omctfn  13051  nninfdclemp1  13058  ptex  13334  fngsum  13458  igsumvalx  13459  isbasis2g  14756  tgval2  14762  ntreq0  14843  bdcuni  16381  bj-axun2  16420