Definition df-rex 3144

Description: Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22.

Note: This notation is most often used to express that 𝜑 holds for at least one element of a given class 𝐴. For this reading Ⅎ𝑥𝐴 is required, though, for example, asserted when 𝑥 and 𝐴 are disjoint.

Should instead 𝐴 depend on 𝑥, you rather assert at least one 𝑥 fulfilling 𝜑 happens to be contained in the corresponding 𝐴(𝑥). This interpretation is rarely needed (see also df-ral 3143). (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 3139	. 2 wff ∃𝑥 ∈ 𝐴 𝜑
5	2	cv 1536	. . . . 5 class 𝑥
6	5, 3	wcel 2114	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 398	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wex 1780	. 2 wff ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 208	1 wff (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  ralnex  3236  rexex  3240  reximi2  3244  rexbii2  3245  rexcom4  3249  rexanidOLD  3253  risset  3267  reximdv2  3271  rexbidv2  3295  rspe  3304  nfre1  3306  reximd2a  3312  r19.23t  3313  rexbida  3318  ralrexbid  3322  r19.12  3324  r19.41v  3347  r19.41  3348  rexcom  3355  reeanlem  3365  rexeqf  3398  reu5  3430  rmo5  3434  cbvrexvw  3450  cbvrexdva2  3457  cbvrexdva2OLD  3458  rexv  3520  2gencl  3535  3gencl  3536  rspce  3612  ceqsrexv  3649  rexab  3686  rexab2  3691  rexab2OLD  3692  rexrab2  3693  morex  3710  reu2  3716  reu6  3717  reu3  3718  2reuswap  3737  2reuswap2  3738  2reu5lem3  3748  2reu5  3749  2rmoswap  3752  ssrexf  4031  rexdifi  4122  rexun  4166  reuss2  4283  reuun2  4286  reupick  4287  reupick3  4288  euelss  4290  reximdva0  4312  n0rex  4314  n0el  4321  r19.2z  4440  r19.2zb  4441  rexsns  4609  exsnrex  4618  dfuni2  4840  eluni2  4842  elunirab  4854  iuncom4  4927  iunxiun  5019  axrep6  5197  axsepgfromrep  5201  intexrab  5243  opeliunxp  5619  xpiundi  5622  xpiundir  5623  ssrelrn  5763  dmuni  5783  rnmpt  5827  elrnmpt1  5830  dfima2  5931  dfima3  5932  elima2  5935  dfco2a  6099  imaco  6104  elsnxp  6142  dffo4  6869  dffo5  6870  abrexco  7003  isomin  7090  zfrep6  7656  opabex3d  7666  opabex3rd  7667  opabex3  7668  abexssex  7671  abexex  7672  frxp  7820  dfrecs3  8009  rdglim2  8068  oarec  8188  oeeu  8229  mapsnd  8450  mapsnend  8588  pssnn  8736  unblem2  8771  dffi2  8887  marypha2lem4  8902  marypha2  8903  zfregcl  9058  axinf2  9103  zfinf2  9105  rankuni  9292  scott0  9315  cp  9320  bnd2  9322  infpwfien  9488  aceq1  9543  dfac5lem2  9550  dfac5lem3  9551  dfac2b  9556  kmlem3  9578  kmlem6  9581  kmlem8  9583  kmlem14  9589  infmap2  9640  ackbij2  9665  cfub  9671  cfval2  9682  cflim3  9684  cfss  9687  cfslb  9688  isf32lem9  9783  zorn2lem6  9923  iundom2g  9962  winalim2  10118  grothprim  10256  genpass  10431  nqpr  10436  1idpr  10451  ltexprlem4  10461  ltexprlem5  10462  reclem2pr  10470  axrrecex  10585  dedekind  10803  sup2  11597  infm3  11600  nnunb  11894  2rexuz  12301  nnwos  12316  xrsupsslem  12701  xrinfmsslem  12702  hashgt23el  13786  ishashinf  13822  cshwsexa  14186  wwlktovfo  14322  maxprmfct  16053  vdwapun  16310  vdwmc  16314  vdwmc2  16315  ram0  16358  imasleval  16814  mreexexlem2d  16916  dfiso2  17042  isssc  17090  drsdirfi  17548  dirge  17847  pwmnd  18102  psgnunilem4  18625  odcau  18729  ablfac2  19211  lspprat  19925  lidlnz  20001  isbasis2g  21556  tgval2  21564  ntreq0  21685  neitr  21788  cmpfi  22016  is1stc2  22050  2ndcsb  22057  2ndcsep  22067  1stcelcls  22069  hausmapdom  22108  isfbas2  22443  fbssint  22446  isfil2  22464  elfg  22479  fgcl  22486  uffix2  22532  alexsubALTlem4  22658  lpbl  23113  metustexhalf  23166  metuel2  23175  restmetu  23180  bcthlem5  23931  upgrex  26877  uvtx01vtx  27179  uhgrvd00  27316  wlkswwlksf1o  27657  wwlksnextsurj  27678  frcond3  28048  frgr3vlem2  28053  3vfriswmgrlem  28056  frgrncvvdeqlem9  28086  ubthlem1  28647  axhcompl-zf  28775  isch3  29018  shne0i  29225  cnlnssadj  29857  reuxfrdf  30255  rexunirn  30256  rmoxfrd  30257  dmrab  30260  abrexdomjm  30267  abrexexd  30269  iunrnmptss  30317  1stpreimas  30441  fpwrelmapffslem  30468  qsxpid  30927  krull  30980  ordtconnlem1  31167  ddemeas  31495  omssubaddlem  31557  omssubadd  31558  eulerpartlemgvv  31634  tgoldbachgt  31934  bnj168  32000  bnj956  32048  bnj1098  32055  bnj1143  32062  bnj1146  32063  bnj1185  32065  bnj1196  32066  bnj600  32191  bnj849  32197  bnj906  32202  bnj916  32205  bnj983  32223  bnj984  32224  bnj1083  32250  bnj1176  32277  bnj1186  32279  bnj1189  32281  bnj1228  32283  bnj1253  32289  bnj1398  32306  bnj1463  32327  bnj1312  32330  bnj1514  32335  exdifsn  32345  lfuhgr3  32366  cusgredgex  32368  loop1cycl  32384  erdszelem10  32447  ptpconn  32480  coep  32987  coepr  32988  dffr5  32989  dfpo2  32991  opelco3  33018  dfon2lem8  33035  brimg  33398  dfrecs2  33411  dfrdg4  33412  ellines  33613  neifg  33719  bj-rexvw  34199  bj-snglc  34284  bj-snglss  34285  bj-rest10  34382  bj-restn0  34384  bj-restpw  34386  bj-rest0  34387  bj-restb  34388  bj-restuni  34391  bj-dfmpoa  34413  bj-finsumval0  34570  rnmptsn  34619  f1omptsnlem  34620  mptsnunlem  34622  topdifinffinlem  34631  isbasisrelowllem1  34639  isbasisrelowllem2  34640  relowlpssretop  34648  fvineqsneq  34696  pibt2  34701  poimirlem30  34937  abrexdom  35020  prdstotbnd  35087  eldmqsres2  35559  exanres  35567  rncnvepres  35576  rnxrnres  35662  1cossres  35689  eldm1cossres  35715  eldmqs1cossres  35908  prtlem17  36027  prter2  36032  islshpat  36168  lsat0cv  36184  lshpsmreu  36260  atex  36557  islpln5  36686  islvol5  36730  pmapglb  36921  pmapglb2N  36922  pmapglb2xN  36923  elpaddn0  36951  pmapjat1  37004  polval2N  37057  osumcllem11N  37117  pexmidlem8N  37128  cdlemftr3  37716  dibelval3  38298  dibglbN  38317  dicelval3  38331  dihglbcpreN  38451  dihglb2  38493  dihjatcclem4  38572  mapdordlem2  38788  mapdrvallem2  38796  mapdpglem3  38826  hdmapglem7a  39078  imaopab  39168  prjspeclsp  39311  rp-isfinite5  39932  rp-isfinite6  39933  elintima  40047  iunrelexpuztr  40113  cotrclrcl  40136  neik0pk1imk0  40446  ntrneineine0lem  40482  ntrneineine1lem  40483  ntrneiel2  40485  cpcolld  40643  expandrexn  40676  ismnuprim  40679  rr-grothprimbi  40680  rr-groth  40684  rexbidar  40827  onfrALTlem5  40925  onfrALTlem2  40929  onfrALTlem1  40931  onfrALTlem5VD  41268  onfrALTlem2VD  41272  onfrALTlem1VD  41273  chordthmALT  41316  rspcegf  41329  cncmpmax  41338  rfcnnnub  41342  inn0f  41384  nssrex  41400  eluni2f  41418  eliin2f  41419  suprnmpt  41479  founiiun0  41500  disjinfi  41503  fvelima2  41581  ssfiunibd  41625  infrpge  41668  fsumiunss  41905  islpcn  41969  lptre2pt  41970  stoweidlem14  42348  stoweidlem34  42368  stoweidlem35  42369  stoweidlem43  42377  stoweidlem44  42378  stoweidlem50  42384  stoweidlem54  42388  stoweidlem56  42390  stoweidlem59  42393  stoweidlem60  42394  fourier2  42561  qndenserrnbllem  42628  qndenserrn  42633  sge0rpcpnf  42752  hoidmvval0b  42921  hoiqssbllem3  42955  imasetpreimafvbijlemfv1  43612  nfermltl8rev  43956  nfermltl2rev  43957  nfermltlrev  43958  nn0mnd  44135  opeliun2xp  44430  setrec1lem3  44841