Definition df-rex 2491

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

This definition is referenced by:  ralnex  2495  rexnalim  2496  dfrex2dc  2498  rexbida  2502  rexbidv2  2510  rexbid2  2512  rexbii2  2518  r2exf  2525  risset  2535  nfrexdxy  2541  nfrexdya  2543  nfre1  2550  rexex  2553  rspe  2556  rsp2e  2558  rexim  2601  reximi2  2603  reximdv2  2606  r19.23t  2614  r19.41  2662  r19.43  2665  reean  2676  rexeqf  2700  reu5  2724  rmo5  2727  cbvrexfw  2730  cbvrexf  2732  cbvrexvw  2744  cbvrexdva2  2747  rexv  2791  2gencl  2806  3gencl  2807  rspce  2873  rspcimedv  2880  ceqsrexv  2904  rexab  2936  rexab2  2940  rexrab2  2941  morex  2958  reu2  2962  reu6  2963  reu3  2964  2reuswapdc  2978  2rmorex  2980  cbvrexcsf  3158  ssrexf  3256  rexun  3354  reuss2  3454  reuun2  3457  reupick  3458  reupick3  3459  reximdva0m  3477  rabn0r  3488  rabn0m  3489  r19.2m  3548  r19.2mOLD  3549  r19.9rmv  3553  rexm  3561  rexsns  3673  exsnrex  3676  dfuni2  3854  eluni2  3856  elunirab  3865  iuncom4  3936  iunxiun  4011  intexrabim  4201  bnd2  4221  rexxfrd  4514  elxp2  4697  opeliunxp  4734  xpiundi  4737  xpiundir  4738  rexiunxp  4824  ssrelrn  4874  dmuni  4893  rnmpt  4931  elrnmpt1  4934  elres  5000  dfima2  5029  dfima3  5030  elima2  5033  dfco2a  5188  imaco  5193  imadiflem  5358  imadif  5359  imainlem  5360  imain  5361  funimaexglem  5362  fvelrnb  5633  rexrnmpt  5730  dffo4  5735  dffo5  5736  abrexco  5835  opabex3d  6213  opabex3  6214  abexssex  6217  abexex  6218  ecexr  6632  mapsn  6784  mapsnen  6910  fimax2gtri  7005  ctssdccl  7220  ltexnqq  7528  subhalfnqq  7534  ltbtwnnq  7536  nqnq0  7561  prnmaxl  7608  prnminu  7609  prarloc  7623  genpdflem  7627  genpassl  7644  genpassu  7645  nqprm  7662  nqprl  7671  nqpru  7672  ltsopr  7716  ltexprlemm  7720  ltexprlemloc  7727  suplocexprlemrl  7837  suplocexprlemloc  7841  axprecex  8000  axpre-ltirr  8002  sup3exmid  9037  2rexuz  9710  ioom  10410  nnwosdc  12404  4sqlemafi  12762  inffinp1  12844  omctfn  12858  nninfdclemp1  12865  ptex  13140  fngsum  13264  igsumvalx  13265  isbasis2g  14561  tgval2  14567  ntreq0  14648  bdcuni  15886  bj-axun2  15925