Definition df-rex 2481

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

This definition is referenced by:  ralnex  2485  rexnalim  2486  dfrex2dc  2488  rexbida  2492  rexbidv2  2500  rexbid2  2502  rexbii2  2508  r2exf  2515  risset  2525  nfrexdxy  2531  nfrexdya  2533  nfre1  2540  rexex  2543  rspe  2546  rsp2e  2548  rexim  2591  reximi2  2593  reximdv2  2596  r19.23t  2604  r19.41  2652  r19.43  2655  reean  2666  rexeqf  2690  reu5  2714  rmo5  2717  cbvrexfw  2720  cbvrexf  2722  cbvrexvw  2734  cbvrexdva2  2737  rexv  2781  2gencl  2796  3gencl  2797  rspce  2863  rspcimedv  2870  ceqsrexv  2894  rexab  2926  rexab2  2930  rexrab2  2931  morex  2948  reu2  2952  reu6  2953  reu3  2954  2reuswapdc  2968  2rmorex  2970  cbvrexcsf  3148  ssrexf  3246  rexun  3344  reuss2  3444  reuun2  3447  reupick  3448  reupick3  3449  reximdva0m  3467  rabn0r  3478  rabn0m  3479  r19.2m  3538  r19.2mOLD  3539  r19.9rmv  3543  rexm  3551  rexsns  3662  exsnrex  3665  dfuni2  3842  eluni2  3844  elunirab  3853  iuncom4  3924  iunxiun  3999  intexrabim  4187  bnd2  4207  rexxfrd  4499  elxp2  4682  opeliunxp  4719  xpiundi  4722  xpiundir  4723  rexiunxp  4809  dmuni  4877  rnmpt  4915  elrnmpt1  4918  elres  4983  dfima2  5012  dfima3  5013  elima2  5016  dfco2a  5171  imaco  5176  imadiflem  5338  imadif  5339  imainlem  5340  imain  5341  funimaexglem  5342  fvelrnb  5611  rexrnmpt  5708  dffo4  5713  dffo5  5714  abrexco  5809  opabex3d  6187  opabex3  6188  abexssex  6191  abexex  6192  ecexr  6606  mapsn  6758  mapsnen  6879  fimax2gtri  6971  ctssdccl  7186  ltexnqq  7492  subhalfnqq  7498  ltbtwnnq  7500  nqnq0  7525  prnmaxl  7572  prnminu  7573  prarloc  7587  genpdflem  7591  genpassl  7608  genpassu  7609  nqprm  7626  nqprl  7635  nqpru  7636  ltsopr  7680  ltexprlemm  7684  ltexprlemloc  7691  suplocexprlemrl  7801  suplocexprlemloc  7805  axprecex  7964  axpre-ltirr  7966  sup3exmid  9001  2rexuz  9673  ioom  10367  nnwosdc  12231  4sqlemafi  12589  inffinp1  12671  omctfn  12685  nninfdclemp1  12692  ptex  12966  fngsum  13090  igsumvalx  13091  isbasis2g  14365  tgval2  14371  ntreq0  14452  bdcuni  15606  bj-axun2  15645