Definition df-rex 3063

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 3053). (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 3062	. 2 wff ∃𝑥 ∈ 𝐴 𝜑
5	2	cv 1541	. . . . 5 class 𝑥
6	5, 3	wcel 2114	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wex 1781	. 2 wff ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 206	1 wff (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  ralnex  3064  rexex  3068  rextru  3069  reximi2  3071  rexbii2  3081  rexlimiva  3131  reximdv2  3148  rexbidv2  3158  r19.41v  3168  r3ex  3177  reeanlem  3209  risset  3213  cbvrexvw  3217  rspe  3228  r19.23t  3234  r19.41  3242  reximd2a  3248  rexbida  3250  nfre1  3263  rexcom4  3265  r19.12  3287  rexeq  3294  rexeqfOLD  3329  reu5  3354  rmo5  3370  rexv  3470  2gencl  3485  3gencl  3486  rspce  3567  ceqsrexv  3611  rexab2  3659  rexrab2  3660  morex  3679  reu2  3685  reu6  3686  reu3  3687  2reuswap  3706  2reuswap2  3707  2reu5lem3  3717  2reu5  3718  2rmoswap  3721  ssrexf  4002  ssrexv  4005  rexss  4011  rexdifi  4104  rexun  4150  reuun2  4279  reuss2  4280  reupick  4283  reupick3  4284  euelss  4286  reximdva0  4309  n0rex  4311  n0el  4318  inn0f  4325  r19.2z  4454  rexsns  4630  exsnrex  4639  dfuni2  4867  eluni2  4869  elunirab  4880  iuncom4  4957  iunxiun  5054  axrep6  5235  axrep6OLD  5236  replem  5237  axsepgfromrep  5243  intexrab  5296  opeliunxp  5701  opeliun2xp  5702  xpiundi  5705  xpiundir  5706  ssrelrn  5853  dmuni  5873  rnmpt  5916  elrnmpt1  5919  dfima2  6031  dfima3  6032  elima2  6035  dfco2a  6214  imaco  6219  elsnxp  6259  dfpo2  6264  fvelima2  6896  dffo4  7059  dffo5  7060  abrexco  7202  isomin  7295  imaeqsexvOLD  7321  imaeqexov  7608  zfrep6OLD  7911  opabex3d  7921  opabex3rd  7922  opabex3  7923  abexssex  7926  abexex  7927  frxp  8080  dfrecs3  8316  rdglim2  8375  oarec  8501  oeeu  8543  mapsnd  8838  mapsnend  8987  pssnn  9107  enfii  9124  enp1i  9193  unblem2  9207  pwfir  9231  dffi2  9340  marypha2lem4  9355  marypha2  9356  zfregcl  9513  zfregclOLD  9514  axinf2  9563  zfinf2  9565  brttrcl2  9637  ttrclselem2  9649  rankuni  9789  scott0  9812  cp  9817  bnd2  9819  infpwfien  9986  aceq1  10041  dfac5lem2  10048  dfac5lem3  10049  dfac2b  10055  kmlem3  10077  kmlem6  10080  kmlem8  10082  kmlem14  10088  infmap2  10141  ackbij2  10166  cfub  10173  cfval2  10184  cflim3  10186  cfss  10189  cfslb  10190  isf32lem9  10285  zorn2lem6  10425  iundom2g  10464  winalim2  10621  grothprim  10759  genpass  10934  nqpr  10939  1idpr  10954  ltexprlem4  10964  ltexprlem5  10965  reclem2pr  10973  axrrecex  11088  dedekind  11310  sup2  12112  infm3  12115  nnunb  12411  2rexuz  12827  nnwos  12842  xrsupsslem  13236  xrinfmsslem  13237  hashgt23el  14361  ishashinf  14400  wwlktovfo  14895  maxprmfct  16650  vdwapun  16916  vdwmc  16920  vdwmc2  16921  ram0  16964  imasleval  17476  mreexexlem2d  17582  dfiso2  17710  isssc  17758  drsdirfi  18242  dirge  18540  pwmnd  18879  psgnunilem4  19443  odcau  19550  ablfac2  20037  lspprat  21125  lidlnz  21214  isbasis2g  22909  tgval2  22917  ntreq0  23038  neitr  23141  cmpfi  23369  is1stc2  23403  2ndcsb  23410  2ndcsep  23420  1stcelcls  23422  hausmapdom  23461  isfbas2  23796  fbssint  23799  isfil2  23817  elfg  23832  fgcl  23839  uffix2  23885  alexsubALTlem4  24011  lpbl  24464  metustexhalf  24517  metuel2  24526  restmetu  24531  bcthlem5  25301  lrrecfr  27956  upgrex  29183  uvtx01vtx  29488  uhgrvd00  29626  wlkswwlksf1o  29970  wwlksnextsurj  29991  frcond3  30362  frgr3vlem2  30367  3vfriswmgrlem  30370  frgrncvvdeqlem9  30400  ubthlem1  30964  axhcompl-zf  31092  isch3  31335  shne0i  31542  cnlnssadj  32174  reuxfrdf  32583  rexunirn  32584  rmoxfrd  32585  dmrab  32589  abrexdomjm  32600  abrexexd  32602  iunrnmptss  32658  ac6mapd  32719  1stpreimas  32802  fpwrelmapffslem  32828  qsxpid  33461  krull  33578  zarclsint  34056  ordtconnlem1  34108  ddemeas  34420  omssubaddlem  34483  omssubadd  34484  eulerpartlemgvv  34560  tgoldbachgt  34847  bnj168  34913  bnj956  34959  bnj1098  34966  bnj1143  34972  bnj1146  34973  bnj1185  34975  bnj1196  34976  bnj600  35101  bnj849  35107  bnj906  35112  bnj916  35115  bnj983  35133  bnj984  35134  bnj1083  35160  bnj1176  35187  bnj1186  35189  bnj1189  35191  bnj1228  35193  bnj1253  35199  bnj1398  35216  bnj1463  35237  bnj1312  35240  bnj1514  35245  exdifsn  35261  r1filimi  35286  axprALT2  35293  axregszf  35313  onvf1odlem1  35325  onvf1odlem2  35326  wevgblacfn  35331  lfuhgr3  35342  cusgredgex  35344  loop1cycl  35359  erdszelem10  35422  ptpconn  35455  rexxfr3dALT  35861  coep  35974  coepr  35975  dffr5  35976  opelco3  35997  dfon2lem8  36010  brimg  36157  dfrecs2  36172  dfrdg4  36173  ellines  36374  cbvrexvw2  36449  neifg  36593  regsfromunir1  36698  bj-rexvw  37155  bj-gabima  37215  bj-snglc  37244  bj-snglss  37245  bj-axseprep  37349  bj-axreprepsep  37350  bj-rest10  37368  bj-restn0  37370  bj-restpw  37372  bj-rest0  37373  bj-restb  37374  bj-restuni  37377  bj-dfmpoa  37398  bj-finsumval0  37567  rnmptsn  37617  f1omptsnlem  37618  mptsnunlem  37620  topdifinffinlem  37629  isbasisrelowllem1  37637  isbasisrelowllem2  37638  relowlpssretop  37646  fvineqsneq  37694  pibt2  37699  poimirlem30  37930  abrexdom  38010  prdstotbnd  38074  elrnres  38558  eldmqsres2  38574  exanres  38581  rncnvepres  38589  rnxrnres  38702  1cossres  38799  eldm1cossres  38830  eldmqs1cossres  39024  disjlem17  39182  disjdmqscossss  39186  prtlem17  39281  prter2  39286  islshpat  39422  lsat0cv  39438  lshpsmreu  39514  atex  39811  islpln5  39940  islvol5  39984  pmapglb  40175  pmapglb2N  40176  pmapglb2xN  40177  elpaddn0  40205  pmapjat1  40258  polval2N  40311  osumcllem11N  40371  pexmidlem8N  40382  cdlemftr3  40970  dibelval3  41552  dibglbN  41571  dicelval3  41585  dihglbcpreN  41705  dihglb2  41747  dihjatcclem4  41826  mapdrvallem2  42050  mapdpglem3  42080  hdmapglem7a  42332  sticksstones3  42547  imaopab  42632  sn-sup2  42890  fimgmcyc  42933  prjspeclsp  42999  uniel  43603  nnoeomeqom  43698  tfsconcatlem  43722  tfsconcatrn  43728  tfsconcat0i  43731  rp-isfinite5  43902  rp-isfinite6  43903  minregex  43919  elintima  44038  iunrelexpuztr  44104  cotrclrcl  44127  neik0pk1imk0  44432  ntrneineine0lem  44468  ntrneineine1lem  44469  ntrneiel2  44471  cpcolld  44643  expandrexn  44676  ismnuprim  44679  rr-grothprimbi  44680  rr-groth  44684  ismnushort  44686  rr-grothshortbi  44688  rexbidar  44830  onfrALTlem5  44927  onfrALTlem2  44931  onfrALTlem1  44933  onfrALTlem5VD  45269  onfrALTlem2VD  45273  onfrALTlem1VD  45274  chordthmALT  45317  rspesbcd  45322  modelaxreplem3  45365  ssclaxsep  45367  permaxrep  45391  nregmodel  45402  rspcegf  45412  cncmpmax  45421  rfcnnnub  45425  nssrex  45474  eluni2f  45491  eliin2f  45492  suprnmpt  45562  founiiun0  45578  disjinfi  45580  ssfiunibd  45700  infrpge  45739  fsumiunss  45964  islpcn  46026  lptre2pt  46027  stoweidlem14  46401  stoweidlem34  46421  stoweidlem35  46422  stoweidlem43  46430  stoweidlem44  46431  stoweidlem50  46437  stoweidlem54  46441  stoweidlem56  46443  stoweidlem59  46446  stoweidlem60  46447  fourier2  46614  qndenserrnbllem  46681  qndenserrn  46686  sge0rpcpnf  46808  hoidmvval0b  46977  hoiqssbllem3  47011  chnsubseqword  47265  imasetpreimafvbijlemfv1  47792  nfermltl8rev  48131  nfermltl2rev  48132  nfermltlrev  48133  isubgredg  48255  gpg5edgnedg  48519  nn0mnd  48568  opncldeqv  49290  opnneilv  49297  setrec1lem3  50077