Definition df-rex 3068

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 3059). (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 3067	. 2 wff ∃𝑥 ∈ 𝐴 𝜑
5	2	cv 1535	. . . . 5 class 𝑥
6	5, 3	wcel 2105	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wex 1775	. 2 wff ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 206	1 wff (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  ralnex  3069  rexex  3073  rextru  3074  reximi2  3076  rexbii2  3087  ralrexbidOLD  3104  rexlimiva  3144  reximdv2  3161  rexbidv2  3172  r19.41v  3186  r3ex  3195  reeanlem  3225  risset  3230  cbvrexvw  3235  rspe  3246  r19.23t  3252  r19.41  3260  reximd2a  3266  rexbida  3269  nfre1  3282  rexcom4  3285  rexcomOLD  3288  r19.12  3311  r19.12OLD  3312  rexeq  3319  cbvrexdva2OLD  3347  rexeqfOLD  3352  reu5  3379  rmo5  3397  rexv  3506  2gencl  3521  3gencl  3522  rspce  3610  ceqsrexv  3654  rexabOLD  3703  rexab2  3707  rexrab2  3708  morex  3727  reu2  3733  reu6  3734  reu3  3735  2reuswap  3754  2reuswap2  3755  2reu5lem3  3765  2reu5  3766  2rmoswap  3769  ssrexf  4061  ssrexv  4064  rexdifi  4159  rexun  4205  reuun2  4330  reuss2  4331  reupick  4334  reupick3  4335  euelss  4337  reximdva0  4360  n0rex  4362  n0el  4369  inn0f  4376  r19.2z  4500  r19.2zb  4501  rexsns  4675  exsnrex  4684  dfuni2  4913  eluni2  4915  elunirab  4926  iuncom4  5004  iunxiun  5101  axrep6  5293  axrep6OLD  5294  axsepgfromrep  5299  intexrab  5352  opeliunxp  5755  xpiundi  5758  xpiundir  5759  ssrelrn  5907  dmuni  5927  rnmpt  5970  elrnmpt1  5973  dfima2  6081  dfima3  6082  elima2  6085  dfco2a  6267  imaco  6272  elsnxp  6312  dfpo2  6317  dffo4  7122  dffo5  7123  abrexco  7263  isomin  7356  imaeqsexvOLD  7382  imaeqexov  7670  zfrep6  7977  opabex3d  7988  opabex3rd  7989  opabex3  7990  abexssex  7993  abexex  7994  frxp  8149  dfrecs3  8410  dfrecs3OLD  8411  rdglim2  8470  oarec  8598  oeeu  8639  mapsnd  8924  mapsnend  9074  pssnn  9206  enfii  9223  enp1i  9310  unblem2  9326  pwfir  9352  dffi2  9460  marypha2lem4  9475  marypha2  9476  zfregcl  9631  axinf2  9677  zfinf2  9679  brttrcl2  9751  ttrclselem2  9763  rankuni  9900  scott0  9923  cp  9928  bnd2  9930  infpwfien  10099  aceq1  10154  dfac5lem2  10161  dfac5lem3  10162  dfac2b  10168  kmlem3  10190  kmlem6  10193  kmlem8  10195  kmlem14  10201  infmap2  10254  ackbij2  10279  cfub  10286  cfval2  10297  cflim3  10299  cfss  10302  cfslb  10303  isf32lem9  10398  zorn2lem6  10538  iundom2g  10577  winalim2  10733  grothprim  10871  genpass  11046  nqpr  11051  1idpr  11066  ltexprlem4  11076  ltexprlem5  11077  reclem2pr  11085  axrrecex  11200  dedekind  11421  sup2  12221  infm3  12224  nnunb  12519  2rexuz  12939  nnwos  12954  xrsupsslem  13345  xrinfmsslem  13346  hashgt23el  14459  ishashinf  14498  cshwsexaOLD  14859  wwlktovfo  14993  maxprmfct  16742  vdwapun  17007  vdwmc  17011  vdwmc2  17012  ram0  17055  imasleval  17587  mreexexlem2d  17689  dfiso2  17819  isssc  17867  drsdirfi  18362  dirge  18660  pwmnd  18962  psgnunilem4  19529  odcau  19636  ablfac2  20123  lspprat  21172  lidlnz  21269  isbasis2g  22970  tgval2  22978  ntreq0  23100  neitr  23203  cmpfi  23431  is1stc2  23465  2ndcsb  23472  2ndcsep  23482  1stcelcls  23484  hausmapdom  23523  isfbas2  23858  fbssint  23861  isfil2  23879  elfg  23894  fgcl  23901  uffix2  23947  alexsubALTlem4  24073  lpbl  24531  metustexhalf  24584  metuel2  24593  restmetu  24598  bcthlem5  25375  lrrecfr  27990  upgrex  29123  uvtx01vtx  29428  uhgrvd00  29566  wlkswwlksf1o  29908  wwlksnextsurj  29929  frcond3  30297  frgr3vlem2  30302  3vfriswmgrlem  30305  frgrncvvdeqlem9  30335  ubthlem1  30898  axhcompl-zf  31026  isch3  31269  shne0i  31476  cnlnssadj  32108  reuxfrdf  32518  rexunirn  32519  rmoxfrd  32520  dmrab  32524  abrexdomjm  32534  abrexexd  32536  iunrnmptss  32585  1stpreimas  32720  fpwrelmapffslem  32749  qsxpid  33369  krull  33486  zarclsint  33832  ordtconnlem1  33884  ddemeas  34216  omssubaddlem  34280  omssubadd  34281  eulerpartlemgvv  34357  tgoldbachgt  34656  bnj168  34722  bnj956  34768  bnj1098  34775  bnj1143  34782  bnj1146  34783  bnj1185  34785  bnj1196  34786  bnj600  34911  bnj849  34917  bnj906  34922  bnj916  34925  bnj983  34943  bnj984  34944  bnj1083  34970  bnj1176  34997  bnj1186  34999  bnj1189  35001  bnj1228  35003  bnj1253  35009  bnj1398  35026  bnj1463  35047  bnj1312  35050  bnj1514  35055  exdifsn  35071  wevgblacfn  35092  lfuhgr3  35103  cusgredgex  35105  loop1cycl  35121  erdszelem10  35184  ptpconn  35217  rexxfr3dALT  35623  coep  35731  coepr  35732  dffr5  35733  opelco3  35755  dfon2lem8  35771  brimg  35918  dfrecs2  35931  dfrdg4  35932  ellines  36133  cbvrexvw2  36209  neifg  36353  bj-rexvw  36862  bj-gabima  36922  bj-snglc  36951  bj-snglss  36952  bj-rest10  37070  bj-restn0  37072  bj-restpw  37074  bj-rest0  37075  bj-restb  37076  bj-restuni  37079  bj-dfmpoa  37100  bj-finsumval0  37267  rnmptsn  37317  f1omptsnlem  37318  mptsnunlem  37320  topdifinffinlem  37329  isbasisrelowllem1  37337  isbasisrelowllem2  37338  relowlpssretop  37346  fvineqsneq  37394  pibt2  37399  poimirlem30  37636  abrexdom  37716  prdstotbnd  37780  elrnres  38252  eldmqsres2  38269  exanres  38276  rncnvepres  38284  rnxrnres  38380  1cossres  38410  eldm1cossres  38441  eldmqs1cossres  38640  disjlem17  38780  disjdmqscossss  38784  prtlem17  38857  prter2  38862  islshpat  38998  lsat0cv  39014  lshpsmreu  39090  atex  39388  islpln5  39517  islvol5  39561  pmapglb  39752  pmapglb2N  39753  pmapglb2xN  39754  elpaddn0  39782  pmapjat1  39835  polval2N  39888  osumcllem11N  39948  pexmidlem8N  39959  cdlemftr3  40547  dibelval3  41129  dibglbN  41148  dicelval3  41162  dihglbcpreN  41282  dihglb2  41324  dihjatcclem4  41403  mapdordlem2  41619  mapdrvallem2  41627  mapdpglem3  41657  hdmapglem7a  41909  sticksstones3  42129  imaopab  42248  sn-sup2  42477  fimgmcyc  42520  prjspeclsp  42598  uniel  43205  nnoeomeqom  43301  tfsconcatlem  43325  tfsconcatrn  43331  tfsconcat0i  43334  rp-isfinite5  43506  rp-isfinite6  43507  minregex  43523  elintima  43642  iunrelexpuztr  43708  cotrclrcl  43731  neik0pk1imk0  44036  ntrneineine0lem  44072  ntrneineine1lem  44073  ntrneiel2  44075  cpcolld  44253  expandrexn  44286  ismnuprim  44289  rr-grothprimbi  44290  rr-groth  44294  ismnushort  44296  rr-grothshortbi  44298  rexbidar  44441  onfrALTlem5  44539  onfrALTlem2  44543  onfrALTlem1  44545  onfrALTlem5VD  44882  onfrALTlem2VD  44886  onfrALTlem1VD  44887  chordthmALT  44930  rspesbcd  44935  modelaxreplem3  44944  ssclaxsep  44946  rspcegf  44960  cncmpmax  44969  rfcnnnub  44973  nssrex  45025  eluni2f  45042  eliin2f  45043  suprnmpt  45116  founiiun0  45132  disjinfi  45134  fvelima2  45204  ssfiunibd  45259  infrpge  45300  fsumiunss  45530  islpcn  45594  lptre2pt  45595  stoweidlem14  45969  stoweidlem34  45989  stoweidlem35  45990  stoweidlem43  45998  stoweidlem44  45999  stoweidlem50  46005  stoweidlem54  46009  stoweidlem56  46011  stoweidlem59  46014  stoweidlem60  46015  fourier2  46182  qndenserrnbllem  46249  qndenserrn  46254  sge0rpcpnf  46376  hoidmvval0b  46545  hoiqssbllem3  46579  imasetpreimafvbijlemfv1  47327  nfermltl8rev  47666  nfermltl2rev  47667  nfermltlrev  47668  isubgredg  47789  nn0mnd  48022  opeliun2xp  48177  opncldeqv  48697  opnneilv  48704  setrec1lem3  48919