Definition df-rex 3071

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 3062). (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 3070	. 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  3072  rexex  3076  rextru  3077  reximi2  3079  rexbii2  3090  ralrexbidOLD  3107  rexlimiva  3147  reximdv2  3164  rexbidv2  3175  r19.41v  3189  r3ex  3198  reeanlem  3228  risset  3233  cbvrexvw  3238  rspe  3249  r19.23t  3255  r19.41  3263  reximd2a  3269  rexbida  3272  nfre1  3285  rexcom4  3288  rexcomOLD  3291  r19.12  3314  r19.12OLD  3315  rexeq  3322  cbvrexdva2OLD  3350  rexeqfOLD  3355  reu5  3382  rmo5  3400  rexv  3509  2gencl  3524  3gencl  3525  rspce  3611  ceqsrexv  3655  rexabOLD  3701  rexab2  3705  rexrab2  3706  morex  3725  reu2  3731  reu6  3732  reu3  3733  2reuswap  3752  2reuswap2  3753  2reu5lem3  3763  2reu5  3764  2rmoswap  3767  ssrexf  4050  ssrexv  4053  rexss  4059  rexdifi  4150  rexun  4196  reuun2  4325  reuss2  4326  reupick  4329  reupick3  4330  euelss  4332  reximdva0  4355  n0rex  4357  n0el  4364  inn0f  4371  r19.2z  4495  r19.2zb  4496  rexsns  4671  exsnrex  4680  dfuni2  4909  eluni2  4911  elunirab  4922  iuncom4  5000  iunxiun  5097  axrep6  5288  axrep6OLD  5289  axsepgfromrep  5294  intexrab  5347  opeliunxp  5752  opeliun2xp  5753  xpiundi  5756  xpiundir  5757  ssrelrn  5905  dmuni  5925  rnmpt  5968  elrnmpt1  5971  dfima2  6080  dfima3  6081  elima2  6084  dfco2a  6266  imaco  6271  elsnxp  6311  dfpo2  6316  fvelima2  6961  dffo4  7123  dffo5  7124  abrexco  7264  isomin  7357  imaeqsexvOLD  7383  imaeqexov  7671  zfrep6  7979  opabex3d  7990  opabex3rd  7991  opabex3  7992  abexssex  7995  abexex  7996  frxp  8151  dfrecs3  8412  dfrecs3OLD  8413  rdglim2  8472  oarec  8600  oeeu  8641  mapsnd  8926  mapsnend  9076  pssnn  9208  enfii  9226  enp1i  9313  unblem2  9329  pwfir  9355  dffi2  9463  marypha2lem4  9478  marypha2  9479  zfregcl  9634  axinf2  9680  zfinf2  9682  brttrcl2  9754  ttrclselem2  9766  rankuni  9903  scott0  9926  cp  9931  bnd2  9933  infpwfien  10102  aceq1  10157  dfac5lem2  10164  dfac5lem3  10165  dfac2b  10171  kmlem3  10193  kmlem6  10196  kmlem8  10198  kmlem14  10204  infmap2  10257  ackbij2  10282  cfub  10289  cfval2  10300  cflim3  10302  cfss  10305  cfslb  10306  isf32lem9  10401  zorn2lem6  10541  iundom2g  10580  winalim2  10736  grothprim  10874  genpass  11049  nqpr  11054  1idpr  11069  ltexprlem4  11079  ltexprlem5  11080  reclem2pr  11088  axrrecex  11203  dedekind  11424  sup2  12224  infm3  12227  nnunb  12522  2rexuz  12942  nnwos  12957  xrsupsslem  13349  xrinfmsslem  13350  hashgt23el  14463  ishashinf  14502  cshwsexaOLD  14863  wwlktovfo  14997  maxprmfct  16746  vdwapun  17012  vdwmc  17016  vdwmc2  17017  ram0  17060  imasleval  17586  mreexexlem2d  17688  dfiso2  17816  isssc  17864  drsdirfi  18351  dirge  18648  pwmnd  18950  psgnunilem4  19515  odcau  19622  ablfac2  20109  lspprat  21155  lidlnz  21252  isbasis2g  22955  tgval2  22963  ntreq0  23085  neitr  23188  cmpfi  23416  is1stc2  23450  2ndcsb  23457  2ndcsep  23467  1stcelcls  23469  hausmapdom  23508  isfbas2  23843  fbssint  23846  isfil2  23864  elfg  23879  fgcl  23886  uffix2  23932  alexsubALTlem4  24058  lpbl  24516  metustexhalf  24569  metuel2  24578  restmetu  24583  bcthlem5  25362  lrrecfr  27976  upgrex  29109  uvtx01vtx  29414  uhgrvd00  29552  wlkswwlksf1o  29899  wwlksnextsurj  29920  frcond3  30288  frgr3vlem2  30293  3vfriswmgrlem  30296  frgrncvvdeqlem9  30326  ubthlem1  30889  axhcompl-zf  31017  isch3  31260  shne0i  31467  cnlnssadj  32099  reuxfrdf  32510  rexunirn  32511  rmoxfrd  32512  dmrab  32516  abrexdomjm  32526  abrexexd  32528  iunrnmptss  32578  ac6mapd  32635  1stpreimas  32715  fpwrelmapffslem  32743  qsxpid  33390  krull  33507  zarclsint  33871  ordtconnlem1  33923  ddemeas  34237  omssubaddlem  34301  omssubadd  34302  eulerpartlemgvv  34378  tgoldbachgt  34678  bnj168  34744  bnj956  34790  bnj1098  34797  bnj1143  34804  bnj1146  34805  bnj1185  34807  bnj1196  34808  bnj600  34933  bnj849  34939  bnj906  34944  bnj916  34947  bnj983  34965  bnj984  34966  bnj1083  34992  bnj1176  35019  bnj1186  35021  bnj1189  35023  bnj1228  35025  bnj1253  35031  bnj1398  35048  bnj1463  35069  bnj1312  35072  bnj1514  35077  exdifsn  35093  wevgblacfn  35114  lfuhgr3  35125  cusgredgex  35127  loop1cycl  35142  erdszelem10  35205  ptpconn  35238  rexxfr3dALT  35644  coep  35752  coepr  35753  dffr5  35754  opelco3  35775  dfon2lem8  35791  brimg  35938  dfrecs2  35951  dfrdg4  35952  ellines  36153  cbvrexvw2  36228  neifg  36372  bj-rexvw  36881  bj-gabima  36941  bj-snglc  36970  bj-snglss  36971  bj-rest10  37089  bj-restn0  37091  bj-restpw  37093  bj-rest0  37094  bj-restb  37095  bj-restuni  37098  bj-dfmpoa  37119  bj-finsumval0  37286  rnmptsn  37336  f1omptsnlem  37337  mptsnunlem  37339  topdifinffinlem  37348  isbasisrelowllem1  37356  isbasisrelowllem2  37357  relowlpssretop  37365  fvineqsneq  37413  pibt2  37418  poimirlem30  37657  abrexdom  37737  prdstotbnd  37801  elrnres  38272  eldmqsres2  38289  exanres  38296  rncnvepres  38304  rnxrnres  38400  1cossres  38430  eldm1cossres  38461  eldmqs1cossres  38660  disjlem17  38800  disjdmqscossss  38804  prtlem17  38877  prter2  38882  islshpat  39018  lsat0cv  39034  lshpsmreu  39110  atex  39408  islpln5  39537  islvol5  39581  pmapglb  39772  pmapglb2N  39773  pmapglb2xN  39774  elpaddn0  39802  pmapjat1  39855  polval2N  39908  osumcllem11N  39968  pexmidlem8N  39979  cdlemftr3  40567  dibelval3  41149  dibglbN  41168  dicelval3  41182  dihglbcpreN  41302  dihglb2  41344  dihjatcclem4  41423  mapdordlem2  41639  mapdrvallem2  41647  mapdpglem3  41677  hdmapglem7a  41929  sticksstones3  42149  imaopab  42270  sn-sup2  42501  fimgmcyc  42544  prjspeclsp  42622  uniel  43229  nnoeomeqom  43325  tfsconcatlem  43349  tfsconcatrn  43355  tfsconcat0i  43358  rp-isfinite5  43530  rp-isfinite6  43531  minregex  43547  elintima  43666  iunrelexpuztr  43732  cotrclrcl  43755  neik0pk1imk0  44060  ntrneineine0lem  44096  ntrneineine1lem  44097  ntrneiel2  44099  cpcolld  44277  expandrexn  44310  ismnuprim  44313  rr-grothprimbi  44314  rr-groth  44318  ismnushort  44320  rr-grothshortbi  44322  rexbidar  44465  onfrALTlem5  44562  onfrALTlem2  44566  onfrALTlem1  44568  onfrALTlem5VD  44905  onfrALTlem2VD  44909  onfrALTlem1VD  44910  chordthmALT  44953  rspesbcd  44958  modelaxreplem3  44997  ssclaxsep  44999  rspcegf  45028  cncmpmax  45037  rfcnnnub  45041  nssrex  45091  eluni2f  45108  eliin2f  45109  suprnmpt  45179  founiiun0  45195  disjinfi  45197  ssfiunibd  45321  infrpge  45362  fsumiunss  45590  islpcn  45654  lptre2pt  45655  stoweidlem14  46029  stoweidlem34  46049  stoweidlem35  46050  stoweidlem43  46058  stoweidlem44  46059  stoweidlem50  46065  stoweidlem54  46069  stoweidlem56  46071  stoweidlem59  46074  stoweidlem60  46075  fourier2  46242  qndenserrnbllem  46309  qndenserrn  46314  sge0rpcpnf  46436  hoidmvval0b  46605  hoiqssbllem3  46639  imasetpreimafvbijlemfv1  47390  nfermltl8rev  47729  nfermltl2rev  47730  nfermltlrev  47731  isubgredg  47852  nn0mnd  48095  opncldeqv  48799  opnneilv  48806  setrec1lem3  49208