Definition df-rex 2494

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

This definition is referenced by:  ralnex  2498  rexnalim  2499  dfrex2dc  2501  rexbida  2505  rexbidv2  2513  rexbid2  2515  rexbii2  2521  r2exf  2528  risset  2538  nfrexdxy  2544  nfrexdya  2546  nfre1  2553  rexex  2556  rspe  2559  rsp2e  2561  rexim  2604  reximi2  2606  reximdv2  2609  r19.23t  2618  r19.41  2666  r19.43  2669  reean  2680  rexeqf  2705  reu5  2729  rmo5  2732  cbvrexfw  2735  cbvrexf  2737  cbvrexvw  2750  cbvrexdva2  2753  rexv  2798  2gencl  2813  3gencl  2814  rspce  2882  rspcimedv  2889  ceqsrexv  2913  rexab  2945  rexab2  2949  rexrab2  2950  morex  2967  reu2  2971  reu6  2972  reu3  2973  2reuswapdc  2987  2rmorex  2989  cbvrexcsf  3168  ssrexf  3266  rexun  3364  reuss2  3464  reuun2  3467  reupick  3468  reupick3  3469  reximdva0m  3487  rabn0r  3498  rabn0m  3499  r19.2m  3558  r19.2mOLD  3559  r19.9rmv  3563  rexm  3571  rexsns  3685  exsnrex  3688  dfuni2  3869  eluni2  3871  elunirab  3880  iuncom4  3951  iunxiun  4026  intexrabim  4216  bnd2  4236  rexxfrd  4531  elxp2  4714  opeliunxp  4751  xpiundi  4754  xpiundir  4755  rexiunxp  4841  ssrelrn  4891  dmuni  4910  rnmpt  4948  elrnmpt1  4951  elres  5017  dfima2  5046  dfima3  5047  elima2  5050  dfco2a  5205  imaco  5210  imadiflem  5376  imadif  5377  imainlem  5378  imain  5379  funimaexglem  5380  fvelrnb  5654  rexrnmpt  5751  dffo4  5756  dffo5  5757  abrexco  5856  opabex3d  6236  opabex3  6237  abexssex  6240  abexex  6241  ecexr  6655  mapsn  6807  mapsnen  6934  fimax2gtri  7031  ctssdccl  7246  ltexnqq  7563  subhalfnqq  7569  ltbtwnnq  7571  nqnq0  7596  prnmaxl  7643  prnminu  7644  prarloc  7658  genpdflem  7662  genpassl  7679  genpassu  7680  nqprm  7697  nqprl  7706  nqpru  7707  ltsopr  7751  ltexprlemm  7755  ltexprlemloc  7762  suplocexprlemrl  7872  suplocexprlemloc  7876  axprecex  8035  axpre-ltirr  8037  sup3exmid  9072  2rexuz  9745  ioom  10447  nnwosdc  12526  4sqlemafi  12884  inffinp1  12966  omctfn  12980  nninfdclemp1  12987  ptex  13263  fngsum  13387  igsumvalx  13388  isbasis2g  14684  tgval2  14690  ntreq0  14771  bdcuni  16149  bj-axun2  16188