Definition df-rex 2478

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

This definition is referenced by:  ralnex  2482  rexnalim  2483  dfrex2dc  2485  rexbida  2489  rexbidv2  2497  rexbid2  2499  rexbii2  2505  r2exf  2512  risset  2522  nfrexdxy  2528  nfrexdya  2530  nfre1  2537  rexex  2540  rspe  2543  rsp2e  2545  rexim  2588  reximi2  2590  reximdv2  2593  r19.23t  2601  r19.41  2649  r19.43  2652  reean  2663  rexeqf  2687  reu5  2711  rmo5  2714  cbvrexfw  2717  cbvrexf  2719  cbvrexvw  2731  cbvrexdva2  2734  rexv  2778  2gencl  2793  3gencl  2794  rspce  2859  rspcimedv  2866  ceqsrexv  2890  rexab  2922  rexab2  2926  rexrab2  2927  morex  2944  reu2  2948  reu6  2949  reu3  2950  2reuswapdc  2964  2rmorex  2966  cbvrexcsf  3144  ssrexf  3241  rexun  3339  reuss2  3439  reuun2  3442  reupick  3443  reupick3  3444  reximdva0m  3462  rabn0r  3473  rabn0m  3474  r19.2m  3533  r19.2mOLD  3534  r19.9rmv  3538  rexm  3546  rexsns  3657  exsnrex  3660  dfuni2  3837  eluni2  3839  elunirab  3848  iuncom4  3919  iunxiun  3994  intexrabim  4182  bnd2  4202  rexxfrd  4494  elxp2  4677  opeliunxp  4714  xpiundi  4717  xpiundir  4718  rexiunxp  4804  dmuni  4872  rnmpt  4910  elrnmpt1  4913  elres  4978  dfima2  5007  dfima3  5008  elima2  5011  dfco2a  5166  imaco  5171  imadiflem  5333  imadif  5334  imainlem  5335  imain  5336  funimaexglem  5337  fvelrnb  5604  rexrnmpt  5701  dffo4  5706  dffo5  5707  abrexco  5802  opabex3d  6173  opabex3  6174  abexssex  6177  abexex  6178  ecexr  6592  mapsn  6744  mapsnen  6865  fimax2gtri  6957  ctssdccl  7170  ltexnqq  7468  subhalfnqq  7474  ltbtwnnq  7476  nqnq0  7501  prnmaxl  7548  prnminu  7549  prarloc  7563  genpdflem  7567  genpassl  7584  genpassu  7585  nqprm  7602  nqprl  7611  nqpru  7612  ltsopr  7656  ltexprlemm  7660  ltexprlemloc  7667  suplocexprlemrl  7777  suplocexprlemloc  7781  axprecex  7940  axpre-ltirr  7942  sup3exmid  8976  2rexuz  9647  ioom  10329  nnwosdc  12176  4sqlemafi  12533  inffinp1  12586  omctfn  12600  nninfdclemp1  12607  ptex  12875  fngsum  12971  igsumvalx  12972  isbasis2g  14213  tgval2  14219  ntreq0  14300  bdcuni  15368  bj-axun2  15407