Definition df-rex 3061

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 3052). (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 3060	. 2 wff ∃𝑥 ∈ 𝐴 𝜑
5	2	cv 1539	. . . . 5 class 𝑥
6	5, 3	wcel 2108	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wex 1779	. 2 wff ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 206	1 wff (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  ralnex  3062  rexex  3066  rextru  3067  reximi2  3069  rexbii2  3079  rexlimiva  3133  reximdv2  3150  rexbidv2  3160  r19.41v  3174  r3ex  3183  reeanlem  3212  risset  3217  cbvrexvw  3221  rspe  3232  r19.23t  3238  r19.41  3246  reximd2a  3252  rexbida  3254  nfre1  3267  rexcom4  3269  rexcomOLD  3272  r19.12  3294  rexeq  3301  cbvrexdva2OLD  3329  rexeqfOLD  3334  reu5  3361  rmo5  3379  rexv  3488  2gencl  3503  3gencl  3504  rspce  3590  ceqsrexv  3634  rexab2  3682  rexrab2  3683  morex  3702  reu2  3708  reu6  3709  reu3  3710  2reuswap  3729  2reuswap2  3730  2reu5lem3  3740  2reu5  3741  2rmoswap  3744  ssrexf  4025  ssrexv  4028  rexss  4034  rexdifi  4125  rexun  4171  reuun2  4300  reuss2  4301  reupick  4304  reupick3  4305  euelss  4307  reximdva0  4330  n0rex  4332  n0el  4339  inn0f  4346  r19.2z  4470  r19.2zb  4471  rexsns  4647  exsnrex  4656  dfuni2  4885  eluni2  4887  elunirab  4898  iuncom4  4976  iunxiun  5073  axrep6  5258  axrep6OLD  5259  axsepgfromrep  5264  intexrab  5317  opeliunxp  5721  opeliun2xp  5722  xpiundi  5725  xpiundir  5726  ssrelrn  5874  dmuni  5894  rnmpt  5937  elrnmpt1  5940  dfima2  6049  dfima3  6050  elima2  6053  dfco2a  6235  imaco  6240  elsnxp  6280  dfpo2  6285  fvelima2  6930  dffo4  7092  dffo5  7093  abrexco  7235  isomin  7329  imaeqsexvOLD  7355  imaeqexov  7643  zfrep6  7951  opabex3d  7962  opabex3rd  7963  opabex3  7964  abexssex  7967  abexex  7968  frxp  8123  dfrecs3  8384  dfrecs3OLD  8385  rdglim2  8444  oarec  8572  oeeu  8613  mapsnd  8898  mapsnend  9048  pssnn  9180  enfii  9198  enp1i  9283  unblem2  9299  pwfir  9325  dffi2  9433  marypha2lem4  9448  marypha2  9449  zfregcl  9606  axinf2  9652  zfinf2  9654  brttrcl2  9726  ttrclselem2  9738  rankuni  9875  scott0  9898  cp  9903  bnd2  9905  infpwfien  10074  aceq1  10129  dfac5lem2  10136  dfac5lem3  10137  dfac2b  10143  kmlem3  10165  kmlem6  10168  kmlem8  10170  kmlem14  10176  infmap2  10229  ackbij2  10254  cfub  10261  cfval2  10272  cflim3  10274  cfss  10277  cfslb  10278  isf32lem9  10373  zorn2lem6  10513  iundom2g  10552  winalim2  10708  grothprim  10846  genpass  11021  nqpr  11026  1idpr  11041  ltexprlem4  11051  ltexprlem5  11052  reclem2pr  11060  axrrecex  11175  dedekind  11396  sup2  12196  infm3  12199  nnunb  12495  2rexuz  12914  nnwos  12929  xrsupsslem  13321  xrinfmsslem  13322  hashgt23el  14440  ishashinf  14479  cshwsexaOLD  14841  wwlktovfo  14975  maxprmfct  16726  vdwapun  16992  vdwmc  16996  vdwmc2  16997  ram0  17040  imasleval  17553  mreexexlem2d  17655  dfiso2  17783  isssc  17831  drsdirfi  18315  dirge  18611  pwmnd  18913  psgnunilem4  19476  odcau  19583  ablfac2  20070  lspprat  21112  lidlnz  21201  isbasis2g  22884  tgval2  22892  ntreq0  23013  neitr  23116  cmpfi  23344  is1stc2  23378  2ndcsb  23385  2ndcsep  23395  1stcelcls  23397  hausmapdom  23436  isfbas2  23771  fbssint  23774  isfil2  23792  elfg  23807  fgcl  23814  uffix2  23860  alexsubALTlem4  23986  lpbl  24440  metustexhalf  24493  metuel2  24502  restmetu  24507  bcthlem5  25278  lrrecfr  27893  upgrex  29017  uvtx01vtx  29322  uhgrvd00  29460  wlkswwlksf1o  29807  wwlksnextsurj  29828  frcond3  30196  frgr3vlem2  30201  3vfriswmgrlem  30204  frgrncvvdeqlem9  30234  ubthlem1  30797  axhcompl-zf  30925  isch3  31168  shne0i  31375  cnlnssadj  32007  reuxfrdf  32418  rexunirn  32419  rmoxfrd  32420  dmrab  32424  abrexdomjm  32434  abrexexd  32436  iunrnmptss  32492  ac6mapd  32549  1stpreimas  32629  fpwrelmapffslem  32655  qsxpid  33323  krull  33440  zarclsint  33849  ordtconnlem1  33901  ddemeas  34213  omssubaddlem  34277  omssubadd  34278  eulerpartlemgvv  34354  tgoldbachgt  34641  bnj168  34707  bnj956  34753  bnj1098  34760  bnj1143  34767  bnj1146  34768  bnj1185  34770  bnj1196  34771  bnj600  34896  bnj849  34902  bnj906  34907  bnj916  34910  bnj983  34928  bnj984  34929  bnj1083  34955  bnj1176  34982  bnj1186  34984  bnj1189  34986  bnj1228  34988  bnj1253  34994  bnj1398  35011  bnj1463  35032  bnj1312  35035  bnj1514  35040  exdifsn  35056  wevgblacfn  35077  lfuhgr3  35088  cusgredgex  35090  loop1cycl  35105  erdszelem10  35168  ptpconn  35201  rexxfr3dALT  35607  coep  35715  coepr  35716  dffr5  35717  opelco3  35738  dfon2lem8  35754  brimg  35901  dfrecs2  35914  dfrdg4  35915  ellines  36116  cbvrexvw2  36191  neifg  36335  bj-rexvw  36844  bj-gabima  36904  bj-snglc  36933  bj-snglss  36934  bj-rest10  37052  bj-restn0  37054  bj-restpw  37056  bj-rest0  37057  bj-restb  37058  bj-restuni  37061  bj-dfmpoa  37082  bj-finsumval0  37249  rnmptsn  37299  f1omptsnlem  37300  mptsnunlem  37302  topdifinffinlem  37311  isbasisrelowllem1  37319  isbasisrelowllem2  37320  relowlpssretop  37328  fvineqsneq  37376  pibt2  37381  poimirlem30  37620  abrexdom  37700  prdstotbnd  37764  elrnres  38235  eldmqsres2  38252  exanres  38259  rncnvepres  38267  rnxrnres  38363  1cossres  38393  eldm1cossres  38424  eldmqs1cossres  38623  disjlem17  38763  disjdmqscossss  38767  prtlem17  38840  prter2  38845  islshpat  38981  lsat0cv  38997  lshpsmreu  39073  atex  39371  islpln5  39500  islvol5  39544  pmapglb  39735  pmapglb2N  39736  pmapglb2xN  39737  elpaddn0  39765  pmapjat1  39818  polval2N  39871  osumcllem11N  39931  pexmidlem8N  39942  cdlemftr3  40530  dibelval3  41112  dibglbN  41131  dicelval3  41145  dihglbcpreN  41265  dihglb2  41307  dihjatcclem4  41386  mapdordlem2  41602  mapdrvallem2  41610  mapdpglem3  41640  hdmapglem7a  41892  sticksstones3  42107  imaopab  42228  sn-sup2  42461  fimgmcyc  42504  prjspeclsp  42582  uniel  43188  nnoeomeqom  43283  tfsconcatlem  43307  tfsconcatrn  43313  tfsconcat0i  43316  rp-isfinite5  43488  rp-isfinite6  43489  minregex  43505  elintima  43624  iunrelexpuztr  43690  cotrclrcl  43713  neik0pk1imk0  44018  ntrneineine0lem  44054  ntrneineine1lem  44055  ntrneiel2  44057  cpcolld  44230  expandrexn  44263  ismnuprim  44266  rr-grothprimbi  44267  rr-groth  44271  ismnushort  44273  rr-grothshortbi  44275  rexbidar  44418  onfrALTlem5  44515  onfrALTlem2  44519  onfrALTlem1  44521  onfrALTlem5VD  44857  onfrALTlem2VD  44861  onfrALTlem1VD  44862  chordthmALT  44905  rspesbcd  44910  modelaxreplem3  44953  ssclaxsep  44955  permaxrep  44979  rspcegf  44995  cncmpmax  45004  rfcnnnub  45008  nssrex  45058  eluni2f  45075  eliin2f  45076  suprnmpt  45146  founiiun0  45162  disjinfi  45164  ssfiunibd  45286  infrpge  45326  fsumiunss  45552  islpcn  45616  lptre2pt  45617  stoweidlem14  45991  stoweidlem34  46011  stoweidlem35  46012  stoweidlem43  46020  stoweidlem44  46021  stoweidlem50  46027  stoweidlem54  46031  stoweidlem56  46033  stoweidlem59  46036  stoweidlem60  46037  fourier2  46204  qndenserrnbllem  46271  qndenserrn  46276  sge0rpcpnf  46398  hoidmvval0b  46567  hoiqssbllem3  46601  imasetpreimafvbijlemfv1  47365  nfermltl8rev  47704  nfermltl2rev  47705  nfermltlrev  47706  isubgredg  47827  nn0mnd  48102  opncldeqv  48824  opnneilv  48831  setrec1lem3  49501