Definition df-rex 3054

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 3045). (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 3053	. 2 wff ∃𝑥 ∈ 𝐴 𝜑
5	2	cv 1539	. . . . 5 class 𝑥
6	5, 3	wcel 2109	. . . 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  3055  rexex  3059  rextru  3060  reximi2  3062  rexbii2  3072  rexlimiva  3122  reximdv2  3139  rexbidv2  3149  r19.41v  3159  r3ex  3168  reeanlem  3200  risset  3204  cbvrexvw  3208  rspe  3219  r19.23t  3225  r19.41  3233  reximd2a  3239  rexbida  3241  nfre1  3254  rexcom4  3256  r19.12  3279  rexeq  3286  cbvrexdva2OLD  3314  rexeqfOLD  3322  reu5  3347  rmo5  3365  rexv  3466  2gencl  3481  3gencl  3482  rspce  3568  ceqsrexv  3612  rexab2  3661  rexrab2  3662  morex  3681  reu2  3687  reu6  3688  reu3  3689  2reuswap  3708  2reuswap2  3709  2reu5lem3  3719  2reu5  3720  2rmoswap  3723  ssrexf  4004  ssrexv  4007  rexss  4013  rexdifi  4103  rexun  4149  reuun2  4278  reuss2  4279  reupick  4282  reupick3  4283  euelss  4285  reximdva0  4308  n0rex  4310  n0el  4317  inn0f  4324  r19.2z  4448  r19.2zb  4449  rexsns  4625  exsnrex  4634  dfuni2  4863  eluni2  4865  elunirab  4876  iuncom4  4953  iunxiun  5049  axrep6  5230  axrep6OLD  5231  axsepgfromrep  5236  intexrab  5289  opeliunxp  5690  opeliun2xp  5691  xpiundi  5694  xpiundir  5695  ssrelrn  5841  dmuni  5861  rnmpt  5903  elrnmpt1  5906  dfima2  6017  dfima3  6018  elima2  6021  dfco2a  6199  imaco  6204  elsnxp  6243  dfpo2  6248  fvelima2  6879  dffo4  7041  dffo5  7042  abrexco  7184  isomin  7278  imaeqsexvOLD  7304  imaeqexov  7591  zfrep6  7897  opabex3d  7907  opabex3rd  7908  opabex3  7909  abexssex  7912  abexex  7913  frxp  8066  dfrecs3  8302  rdglim2  8361  oarec  8487  oeeu  8528  mapsnd  8820  mapsnend  8968  pssnn  9092  enfii  9110  enp1i  9182  unblem2  9198  pwfir  9224  dffi2  9332  marypha2lem4  9347  marypha2  9348  zfregcl  9505  zfregclOLD  9506  axinf2  9555  zfinf2  9557  brttrcl2  9629  ttrclselem2  9641  rankuni  9778  scott0  9801  cp  9806  bnd2  9808  infpwfien  9975  aceq1  10030  dfac5lem2  10037  dfac5lem3  10038  dfac2b  10044  kmlem3  10066  kmlem6  10069  kmlem8  10071  kmlem14  10077  infmap2  10130  ackbij2  10155  cfub  10162  cfval2  10173  cflim3  10175  cfss  10178  cfslb  10179  isf32lem9  10274  zorn2lem6  10414  iundom2g  10453  winalim2  10609  grothprim  10747  genpass  10922  nqpr  10927  1idpr  10942  ltexprlem4  10952  ltexprlem5  10953  reclem2pr  10961  axrrecex  11076  dedekind  11297  sup2  12099  infm3  12102  nnunb  12398  2rexuz  12819  nnwos  12834  xrsupsslem  13227  xrinfmsslem  13228  hashgt23el  14349  ishashinf  14388  cshwsexaOLD  14749  wwlktovfo  14883  maxprmfct  16638  vdwapun  16904  vdwmc  16908  vdwmc2  16909  ram0  16952  imasleval  17463  mreexexlem2d  17569  dfiso2  17697  isssc  17745  drsdirfi  18229  dirge  18527  pwmnd  18829  psgnunilem4  19394  odcau  19501  ablfac2  19988  lspprat  21078  lidlnz  21167  isbasis2g  22851  tgval2  22859  ntreq0  22980  neitr  23083  cmpfi  23311  is1stc2  23345  2ndcsb  23352  2ndcsep  23362  1stcelcls  23364  hausmapdom  23403  isfbas2  23738  fbssint  23741  isfil2  23759  elfg  23774  fgcl  23781  uffix2  23827  alexsubALTlem4  23953  lpbl  24407  metustexhalf  24460  metuel2  24469  restmetu  24474  bcthlem5  25244  lrrecfr  27873  upgrex  29055  uvtx01vtx  29360  uhgrvd00  29498  wlkswwlksf1o  29842  wwlksnextsurj  29863  frcond3  30231  frgr3vlem2  30236  3vfriswmgrlem  30239  frgrncvvdeqlem9  30269  ubthlem1  30832  axhcompl-zf  30960  isch3  31203  shne0i  31410  cnlnssadj  32042  reuxfrdf  32453  rexunirn  32454  rmoxfrd  32455  dmrab  32459  abrexdomjm  32469  abrexexd  32471  iunrnmptss  32527  ac6mapd  32582  1stpreimas  32662  fpwrelmapffslem  32688  qsxpid  33309  krull  33426  zarclsint  33838  ordtconnlem1  33890  ddemeas  34202  omssubaddlem  34266  omssubadd  34267  eulerpartlemgvv  34343  tgoldbachgt  34630  bnj168  34696  bnj956  34742  bnj1098  34749  bnj1143  34756  bnj1146  34757  bnj1185  34759  bnj1196  34760  bnj600  34885  bnj849  34891  bnj906  34896  bnj916  34899  bnj983  34917  bnj984  34918  bnj1083  34944  bnj1176  34971  bnj1186  34973  bnj1189  34975  bnj1228  34977  bnj1253  34983  bnj1398  35000  bnj1463  35021  bnj1312  35024  bnj1514  35029  exdifsn  35045  axregszf  35063  onvf1odlem1  35075  onvf1odlem2  35076  wevgblacfn  35081  lfuhgr3  35092  cusgredgex  35094  loop1cycl  35109  erdszelem10  35172  ptpconn  35205  rexxfr3dALT  35611  coep  35724  coepr  35725  dffr5  35726  opelco3  35747  dfon2lem8  35763  brimg  35910  dfrecs2  35923  dfrdg4  35924  ellines  36125  cbvrexvw2  36200  neifg  36344  bj-rexvw  36853  bj-gabima  36913  bj-snglc  36942  bj-snglss  36943  bj-rest10  37061  bj-restn0  37063  bj-restpw  37065  bj-rest0  37066  bj-restb  37067  bj-restuni  37070  bj-dfmpoa  37091  bj-finsumval0  37258  rnmptsn  37308  f1omptsnlem  37309  mptsnunlem  37311  topdifinffinlem  37320  isbasisrelowllem1  37328  isbasisrelowllem2  37329  relowlpssretop  37337  fvineqsneq  37385  pibt2  37390  poimirlem30  37629  abrexdom  37709  prdstotbnd  37773  elrnres  38245  eldmqsres2  38261  exanres  38268  rncnvepres  38276  rnxrnres  38370  1cossres  38405  eldm1cossres  38436  eldmqs1cossres  38636  disjlem17  38776  disjdmqscossss  38780  prtlem17  38854  prter2  38859  islshpat  38995  lsat0cv  39011  lshpsmreu  39087  atex  39385  islpln5  39514  islvol5  39558  pmapglb  39749  pmapglb2N  39750  pmapglb2xN  39751  elpaddn0  39779  pmapjat1  39832  polval2N  39885  osumcllem11N  39945  pexmidlem8N  39956  cdlemftr3  40544  dibelval3  41126  dibglbN  41145  dicelval3  41159  dihglbcpreN  41279  dihglb2  41321  dihjatcclem4  41400  mapdordlem2  41616  mapdrvallem2  41624  mapdpglem3  41654  hdmapglem7a  41906  sticksstones3  42121  imaopab  42204  sn-sup2  42464  fimgmcyc  42507  prjspeclsp  42585  uniel  43190  nnoeomeqom  43285  tfsconcatlem  43309  tfsconcatrn  43315  tfsconcat0i  43318  rp-isfinite5  43490  rp-isfinite6  43491  minregex  43507  elintima  43626  iunrelexpuztr  43692  cotrclrcl  43715  neik0pk1imk0  44020  ntrneineine0lem  44056  ntrneineine1lem  44057  ntrneiel2  44059  cpcolld  44231  expandrexn  44264  ismnuprim  44267  rr-grothprimbi  44268  rr-groth  44272  ismnushort  44274  rr-grothshortbi  44276  rexbidar  44419  onfrALTlem5  44516  onfrALTlem2  44520  onfrALTlem1  44522  onfrALTlem5VD  44858  onfrALTlem2VD  44862  onfrALTlem1VD  44863  chordthmALT  44906  rspesbcd  44911  modelaxreplem3  44954  ssclaxsep  44956  permaxrep  44980  nregmodel  44991  rspcegf  45001  cncmpmax  45010  rfcnnnub  45014  nssrex  45064  eluni2f  45081  eliin2f  45082  suprnmpt  45152  founiiun0  45168  disjinfi  45170  ssfiunibd  45291  infrpge  45331  fsumiunss  45557  islpcn  45621  lptre2pt  45622  stoweidlem14  45996  stoweidlem34  46016  stoweidlem35  46017  stoweidlem43  46025  stoweidlem44  46026  stoweidlem50  46032  stoweidlem54  46036  stoweidlem56  46038  stoweidlem59  46041  stoweidlem60  46042  fourier2  46209  qndenserrnbllem  46276  qndenserrn  46281  sge0rpcpnf  46403  hoidmvval0b  46572  hoiqssbllem3  46606  imasetpreimafvbijlemfv1  47388  nfermltl8rev  47727  nfermltl2rev  47728  nfermltlrev  47729  isubgredg  47851  gpg5edgnedg  48115  nn0mnd  48164  opncldeqv  48887  opnneilv  48894  setrec1lem3  49675