Definition df-rex 3087

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 3077). (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 3086	. 2 wff ∃𝑥 ∈ 𝐴 𝜑
5	2	cv 1569	. . . . 5 class 𝑥
6	5, 3	wcel 2145	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 401	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wex 1812	. 2 wff ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 209	1 wff (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is used by:  ralnex  3088  rexex  3092  rextru  3093  reximi2  3095  rexbii2  3105  rexlimiva  3155  reximdv2  3172  rexbidv2  3182  r19.41v  3192  r3ex  3201  reeanlem  3233  risset  3237  cbvrexvw  3241  rspe  3252  r19.23t  3258  r19.41  3266  reximd2a  3272  rexbida  3274  nfre1  3287  rexcom4  3289  r19.12  3311  rexeq  3315  reu5  3367  rmo5  3383  rexv  3477  2gencl  3492  3gencl  3493  rspce  3565  ceqsrexv  3609  rexab2  3657  rexrab2  3658  morex  3677  reu2  3683  reu6  3684  reu3  3685  2reuswap  3704  2reuswap2  3705  2reu5lem3  3715  2reu5  3716  2rmoswap  3719  nssrex  3996  ssrexf  3998  ssrexv  4001  rexss  4005  rexdifi  4097  rexun  4142  reuun2  4271  reuss2  4272  reupick  4275  reupick3  4276  euelss  4278  reximdva0  4303  n0rex  4305  n0el  4312  inn0f  4319  r19.2z  4455  rexsns  4632  exsnrex  4641  dfuni2  4869  eluni2  4871  elunirab  4882  iuncom4  4960  iunxiun  5057  axrep6  5241  axrep6OLD  5242  replem  5243  axsepgfromrep  5249  intexrab  5311  opeliunxp  5722  opeliun2xp  5723  xpiundi  5726  xpiundir  5727  ssrelrn  5878  dmuni  5898  rnmpt  5941  elrnmpt1  5944  dfima2  6058  dfima3  6059  elima2  6062  dfco2a  6242  imaco  6247  elsnxp  6289  dfpo2  6294  fvelima2  6930  dffo4  7096  dffo5  7097  abrexco  7241  isomin  7338  imaeqexov  7652  zfrep6OLD  7952  opabex3d  7962  opabex3rd  7963  opabex3  7964  abexssex  7967  abexex  7968  frxp  8124  dfrecs3  8361  rdglim2  8421  oarec  8549  oeeu  8591  mapsnd  8893  mapsnend  9043  pssnn  9163  enfii  9180  enp1i  9249  unblem2  9263  pwfir  9286  dffi2  9393  marypha2lem4  9408  marypha2  9409  zfregcl  9566  zfregclOLD  9567  axinf2  9619  zfinf2  9621  brttrcl2  9693  ttrclselem2  9705  rankuni  9845  scott0b  9876  scott0OLD  9877  cp  9893  bnd2  9895  infpwfien  10065  aceq1  10120  dfac5lem2  10127  dfac5lem3  10128  dfac2b  10133  kmlem3  10155  kmlem6  10158  kmlem8  10160  kmlem14  10166  infmap2  10219  ackbij2  10244  cfub  10250  cfval2  10262  cflim3  10264  cfss  10267  cfslb  10268  isf32lem9  10363  zorn2lem6  10503  iundom2g  10548  winalim2  10705  grothprim  10843  genpass  11018  nqpr  11023  1idpr  11038  ltexprlem4  11048  ltexprlem5  11049  reclem2pr  11057  axrrecex  11172  dedekind  11397  sup2  12195  infm3  12198  nnunb  12524  2rexuz  12949  nnwos  12964  xrsupsslem  13359  xrinfmsslem  13360  hashgt23el  14489  ishashinf  14528  wwlktovfo  15031  maxprmfct  16800  vdwapun  17066  vdwmc  17070  vdwmc2  17071  ram0  17114  imasleval  17627  mreexexlem2d  17733  dfiso2  17861  isssc  17909  drsdirfi  18393  dirge  18691  pwmnd  19056  qsxpid  19300  psgnunilem4  19624  odcau  19731  ablfac2  20218  lspprat  21340  lidlnz  21439  isbasis2g  23173  tgval2  23181  ntreq0  23302  neitr  23405  cmpfi  23633  is1stc2  23667  2ndcsb  23674  2ndcsep  23685  1stcelcls  23687  hausmapdom  23726  isfbas2  24061  fbssint  24064  isfil2  24082  elfg  24097  fgcl  24104  uffix2  24150  alexsubALTlem4  24276  lpbl  24729  metustexhalf  24782  metuel2  24791  restmetu  24796  bcthlem5  25556  lrrecfr  28208  upgrex  29549  lfuhgr3  29607  uvtx01vtx  29857  uhgrvd00  29994  wlkswwlksf1o  30347  wwlksnextsurj  30368  loop1cycl  30623  frcond3  30749  frgr3vlem2  30754  3vfriswmgrlem  30757  frgrncvvdeqlem9  30787  ubthlem1  31351  axhcompl-zf  31479  isch3  31722  shne0i  31929  cnlnssadj  32561  reuxfrdf  32966  rexunirn  32967  rmoxfrd  32968  dmrab  32972  abrexdomjm  32982  abrexexd  32984  iunrnmptss  33038  ac6mapd  33096  1stpreimas  33178  fpwrelmapffslem  33203  krull  33881  zarclsint  34382  ordtconnlem1  34434  ddemeas  34747  omssubaddlem  34810  omssubadd  34811  eulerpartlemgvv  34887  tgoldbachgt  35171  bnj168  35240  bnj956  35286  bnj1098  35293  bnj1143  35299  bnj1146  35300  bnj1185  35302  bnj1196  35303  bnj600  35428  bnj849  35434  bnj906  35439  bnj916  35442  bnj983  35460  bnj984  35461  bnj1083  35487  bnj1176  35514  bnj1186  35516  bnj1189  35518  bnj1228  35520  bnj1253  35526  bnj1398  35543  bnj1463  35564  bnj1312  35567  bnj1514  35572  exdifsn  35589  r1filimi  35611  axprALT2  35617  axregszf  35655  karddom  35687  kardsdom  35688  kardfi  35696  onvf1odlem1  35700  onvf1odlem2  35701  wevgblacfn  35708  cusgredgex  35720  erdszelem10  35779  ptpconn  35812  rexxfr3dALT  36218  coep  36331  coepr  36332  dffr5  36333  opelco3  36354  dfon2lem8  36367  brimg  36514  dfrecs2  36529  dfrdg4  36530  ellines  36732  cbvrexvw2  36847  neifg  36990  regsfromunir1  37159  bj-rexvw  37623  bj-gabima  37684  bj-snglc  37713  bj-snglss  37714  bj-axseprep  37819  bj-axreprepsep  37820  bj-rest10  37838  bj-restn0  37840  bj-restpw  37842  bj-rest0  37843  bj-restb  37844  bj-restuni  37847  bj-dfmpoa  37868  bj-finsumval0  38037  rnmptsn  38089  f1omptsnlem  38090  mptsnunlem  38092  topdifinffinlem  38101  isbasisrelowllem1  38109  isbasisrelowllem2  38110  relowlpssretop  38118  fvineqsneq  38166  pibt2  38171  poimirlem30  38399  abrexdom  38480  prdstotbnd  38544  elrnres  39026  eldmqsres2  39042  exanres  39049  rncnvepres  39057  rnxrnres  39170  1cossres  39267  eldm1cossres  39298  eldmqs1cossres  39492  disjlem17  39650  disjdmqscossss  39654  prtlem17  39749  prter2  39754  islshpat  39890  lsat0cv  39906  lshpsmreu  39982  atex  40279  islpln5  40408  islvol5  40452  pmapglb  40643  pmapglb2N  40644  pmapglb2xN  40645  elpaddn0  40673  pmapjat1  40726  polval2N  40779  osumcllem11N  40839  pexmidlem8N  40850  cdlemftr3  41438  dibelval3  42020  dibglbN  42039  dicelval3  42053  dihglbcpreN  42173  dihglb2  42215  dihjatcclem4  42294  mapdrvallem2  42518  mapdpglem3  42548  hdmapglem7a  42800  sticksstones3  43014  imaopab  43101  sn-sup2  43379  fimgmcyc  43416  prjspeclsp  43458  uniel  44058  nnoeomeqom  44153  tfsconcatlem  44177  tfsconcatrn  44183  tfsconcat0i  44186  rp-isfinite5  44357  rp-isfinite6  44358  minregex  44374  elintima  44493  iunrelexpuztr  44559  cotrclrcl  44582  neik0pk1imk0  44887  ntrneineine0lem  44923  ntrneineine1lem  44924  ntrneiel2  44926  cpcolld  45082  expandrexn  45115  ismnuprim  45118  rr-grothprimbi  45119  rr-groth  45123  ismnushort  45125  rr-grothshortbi  45127  rexbidar  45269  onfrALTlem5  45365  onfrALTlem2  45369  onfrALTlem1  45371  onfrALTlem5VD  45707  onfrALTlem2VD  45711  onfrALTlem1VD  45712  chordthmALT  45755  rspesbcd  45760  modelaxreplem3  45803  ssclaxsep  45805  permaxrep  45829  nregmodel  45840  rspcegf  45857  cncmpmax  45866  rfcnnnub  45870  eluni2f  45935  eliin2f  45936  suprnmpt  46006  founiiun0  46022  disjinfi  46024  ssfiunibd  46142  infrpge  46181  fsumiunss  46405  islpcn  46467  lptre2pt  46468  stoweidlem14  46842  stoweidlem34  46862  stoweidlem35  46863  stoweidlem43  46871  stoweidlem44  46872  stoweidlem50  46878  stoweidlem54  46882  stoweidlem56  46884  stoweidlem59  46887  stoweidlem60  46888  fourier2  47055  qndenserrnbllem  47122  qndenserrn  47127  sge0rpcpnf  47249  hoidmvval0b  47418  hoiqssbllem3  47452  tmachlem-exagreecover  47774  imasetpreimafvbijlemfv1  48303  nfermltl8rev  48658  nfermltl2rev  48659  nfermltlrev  48660  isubgredg  48782  gpg5edgnedg  49046  nn0mnd  49094  opncldeqv  49828  opnneilv  49835  setrec1lem3  50615  dfrals2  50719