Definition df-rex 2621

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	⊢ (∃x ∈ A φ ↔ ∃x(x ∈ A ∧ φ))

Detailed syntax breakdown of Definition df-rex

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		vx	. . 3 setvar x
3		cA	. . 3 class A
4	1, 2, 3	wrex 2616	. 2 wff ∃x ∈ A φ
5	2	cv 1641	. . . . 5 class x
6	5, 3	wcel 1710	. . . 4 wff x ∈ A
7	6, 1	wa 358	. . 3 wff (x ∈ A ∧ φ)
8	7, 2	wex 1541	. 2 wff ∃x(x ∈ A ∧ φ)
9	4, 8	wb 176	1 wff (∃x ∈ A φ ↔ ∃x(x ∈ A ∧ φ))

This definition is referenced by:  ralnex  2625  rexnal  2626  rexbida  2630  rexbidv2  2638  rexbii2  2644  r2exf  2651  risset  2662  nfre1  2671  rexex  2674  rspe  2676  rsp2e  2678  reximi2  2721  reximdv2  2724  r19.23t  2729  r19.41  2764  reean  2778  rexeqf  2805  reu5  2825  rmo5  2828  cbvrexdva2  2841  rexv  2874  2gencl  2889  3gencl  2890  rspce  2951  ceqsrexv  2973  rexab  3000  rexab2  3004  rexrab2  3005  morex  3021  reu2  3025  reu6  3026  reu3  3027  2reuswap  3039  2reu5lem3  3044  2reu5  3045  rexun  3444  reuss2  3536  reuun2  3539  reupick  3540  reupick3  3541  reximdva0  3562  rabn0  3571  r19.2z  3640  r19.2zb  3641  rexsns  3765  dfuni2  3894  eluni2  3896  elunirab  3905  iuncom4  3977  iunxiun  4049  elpw1  4145  elpw12  4146  elpw11c  4148  elpw121c  4149  elpw131c  4150  elpw141c  4151  elpw151c  4152  elpw161c  4153  elpw171c  4154  elpw181c  4155  elpw191c  4156  elpw1101c  4157  elpw1111c  4158  opkelimagekg  4272  imacok  4283  dfimak2  4299  dfpw12  4302  ndisjrelk  4324  dfpw2  4328  dfaddc2  4382  dfnnc2  4396  elsuc  4414  addcass  4416  nnsucelrlem1  4425  ltfinex  4465  ssfin  4471  eqpwrelk  4479  eqpw1relk  4480  ncfinraiselem2  4481  ncfinlowerlem1  4483  nnpw1ex  4485  eqtfinrelk  4487  evenfinex  4504  oddfinex  4505  evenodddisjlem1  4516  nnadjoinlem1  4520  nnpweqlem1  4523  srelk  4525  sfintfinlem1  4532  tfinnnlem1  4534  spfinex  4538  vfinspss  4552  vfinncsp  4555  dfop2lem1  4574  setconslem1  4732  setconslem2  4733  setconslem3  4734  setconslem4  4735  setconslem6  4737  setconslem7  4738  df1st2  4739  dfswap2  4742  elima2  4756  elima3  4757  elxp2  4803  xpiundi  4818  xpiundir  4819  opeliunxp  4821  dmuni  4915  elimapw1  4945  elimapw12  4946  elimapw13  4947  elimapw11c  4949  dfima4  4953  rnopab2  4969  elres  4996  imadmrn  5009  rnuni  5039  dfco2a  5082  imaco  5087  dfcnv2  5101  iunfopab  5205  fnrnfv  5365  dffo4  5424  dffo5  5425  abrexco  5464  isomin  5497  dmsi  5520  disjex  5824  addcfnex  5825  crossex  5851  pw1fnex  5853  pw1fnf1o  5856  transex  5911  refex  5912  antisymex  5913  connexex  5914  foundex  5915  extex  5916  symex  5917  frds  5936  mapsn  6027  xpassen  6058  enpw1pw  6076  mucex  6134  ncspw1eu  6160  el2c  6192  lecidg  6197  lec0cg  6199  lecncvg  6200  addlec  6209  taddc  6230  tcfnex  6245