Definition df-rex 3094

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 3093). (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 3089	. 2 wff ∃𝑥 ∈ 𝐴 𝜑
5	2	cv 1506	. . . . 5 class 𝑥
6	5, 3	wcel 2050	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 387	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wex 1742	. 2 wff ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 198	1 wff (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  ralnex  3183  rexex  3187  reximi2  3191  rexbii2  3192  rexcom4  3196  rexanidOLD  3199  risset  3213  reximdv2  3216  rexbidv2  3240  rspe  3249  nfre1  3251  reximd2a  3255  r19.23t  3256  rexbida  3261  r19.12  3265  r19.41v  3288  r19.41  3289  rexcom  3296  reeanlem  3306  rexeqf  3338  reu5  3370  rmo5  3374  cbvrexdva2  3388  cbvrexdva2OLD  3389  rexv  3441  2gencl  3456  3gencl  3457  rspce  3530  ceqsrexv  3563  rexab  3602  rexab2  3606  rexrab2  3607  morex  3626  reu2  3630  reu6  3631  reu3  3632  2reuswap  3651  2reuswap2  3652  2reu5lem3  3659  2reu5  3660  2rmoswap  3663  ssrexf  3923  rexun  4056  reuss2  4172  reuun2  4175  reupick  4176  reupick3  4177  euelss  4179  reximdva0  4200  n0rex  4202  n0el  4209  r19.2z  4324  r19.2zb  4325  rexsns  4482  exsnrex  4493  dfuni2  4715  eluni2  4717  elunirab  4725  iuncom4  4801  iunxiun  4886  intexrab  5100  opeliunxp  5470  xpiundi  5473  xpiundir  5474  ssrelrn  5614  dmuni  5633  rnmpt  5671  elrnmpt1  5674  dfima2  5774  dfima3  5775  elima2  5778  dfco2a  5940  imaco  5945  elsnxp  5982  dffo4  6694  dffo5  6695  abrexco  6830  isomin  6915  zfrep6  7470  opabex3d  7480  opabex3rd  7481  opabex3  7482  abexssex  7485  abexex  7486  frxp  7627  dfrecs3  7815  rdglim2  7874  oarec  7991  oeeu  8032  mapsnd  8250  mapsnend  8387  pssnn  8533  unblem2  8568  dffi2  8684  marypha2lem4  8699  marypha2  8700  zfregcl  8855  axinf2  8899  zfinf2  8901  rankuni  9088  scott0  9111  cp  9116  bnd2  9118  infpwfien  9284  aceq1  9339  dfac5lem2  9346  dfac5lem3  9347  dfac2b  9352  kmlem3  9374  kmlem6  9377  kmlem8  9379  kmlem14  9385  infmap2  9440  ackbij2  9465  cfub  9471  cfval2  9482  cflim3  9484  cfss  9487  cfslb  9488  isf32lem9  9583  zorn2lem6  9723  iundom2g  9762  winalim2  9918  grothprim  10056  genpass  10231  nqpr  10236  1idpr  10251  ltexprlem4  10261  ltexprlem5  10262  reclem2pr  10270  axrrecex  10385  dedekind  10605  sup2  11400  infm3  11403  nnunb  11706  2rexuz  12117  nnwos  12132  xrsupsslem  12519  xrinfmsslem  12520  hashgt23el  13601  ishashinf  13637  cshwsexa  14051  wwlktovfo  14186  maxprmfct  15912  vdwapun  16169  vdwmc  16173  vdwmc2  16174  ram0  16217  imasleval  16673  mreexexlem2d  16777  dfiso2  16903  isssc  16951  drsdirfi  17409  dirge  17708  psgnunilem4  18390  odcau  18493  ablfac2  18964  lspprat  19650  lidlnz  19725  isbasis2g  21263  tgval2  21271  ntreq0  21392  neitr  21495  cmpfi  21723  is1stc2  21757  2ndcsb  21764  2ndcsep  21774  1stcelcls  21776  hausmapdom  21815  isfbas2  22150  fbssint  22153  isfil2  22171  elfg  22186  fgcl  22193  uffix2  22239  alexsubALTlem4  22365  lpbl  22819  metustexhalf  22872  metuel2  22881  restmetu  22886  bcthlem5  23637  upgrex  26583  uvtx01vtx  26885  uhgrvd00  27022  wlkswwlksf1o  27368  wwlksnextsurj  27394  wwlksnextsurOLD  27399  frcond3  27806  frgr3vlem2  27811  3vfriswmgrlem  27814  frgrncvvdeqlem9  27844  ubthlem1  28428  axhcompl-zf  28557  isch3  28800  shne0i  29009  cnlnssadj  29641  rexunirn  30040  rmoxfrd  30041  dmrab  30042  abrexdomjm  30049  abrexexd  30051  iunrnmptss  30089  1stpreimas  30196  fpwrelmapffslem  30223  ordtconnlem1  30811  ddemeas  31140  omssubaddlem  31202  omssubadd  31203  eulerpartlemgvv  31279  tgoldbachgt  31582  bnj168  31648  bnj956  31696  bnj1098  31703  bnj1143  31710  bnj1146  31711  bnj1185  31713  bnj1196  31714  bnj600  31838  bnj849  31844  bnj906  31849  bnj916  31852  bnj983  31870  bnj984  31871  bnj1083  31895  bnj1176  31922  bnj1186  31924  bnj1189  31926  bnj1228  31928  bnj1253  31934  bnj1398  31951  bnj1463  31972  bnj1312  31975  bnj1514  31980  exdifsn  31990  erdszelem10  32032  ptpconn  32065  coep  32507  coepr  32508  dffr5  32509  dfpo2  32511  opelco3  32538  dfon2lem8  32555  brimg  32919  dfrecs2  32932  dfrdg4  32933  ellines  33134  neifg  33240  bj-rexvw  33689  bj-snglc  33799  bj-snglss  33800  bj-rest10  33889  bj-restn0  33891  bj-restpw  33893  bj-rest0  33894  bj-restb  33895  bj-restuni  33898  bj-dfmpoa  33919  bj-finsumval0  34030  rnmptsn  34058  f1omptsnlem  34059  mptsnunlem  34061  topdifinffinlem  34070  isbasisrelowllem1  34078  isbasisrelowllem2  34079  relowlpssretop  34087  fvineqsneq  34134  pibt2  34139  poimirlem30  34363  abrexdom  34447  prdstotbnd  34514  eldmqsres2  34988  exanres  34996  rncnvepres  35005  rnxrnres  35092  1cossres  35119  eldm1cossres  35145  eldmqs1cossres  35338  prtlem17  35457  prter2  35462  islshpat  35598  lsat0cv  35614  lshpsmreu  35690  atex  35987  islpln5  36116  islvol5  36160  pmapglb  36351  pmapglb2N  36352  pmapglb2xN  36353  elpaddn0  36381  pmapjat1  36434  polval2N  36487  osumcllem11N  36547  pexmidlem8N  36558  cdlemftr3  37146  dibelval3  37728  dibglbN  37747  dicelval3  37761  dihglbcpreN  37881  dihglb2  37923  dihjatcclem4  38002  mapdordlem2  38218  mapdrvallem2  38226  mapdpglem3  38256  hdmapglem7a  38508  sn-axrep  38552  imaopab  38564  prjspeclsp  38669  rp-isfinite5  39279  rp-isfinite6  39280  relintabex  39303  elintima  39361  iunrelexpuztr  39427  cotrclrcl  39450  neik0pk1imk0  39760  ntrneineine0lem  39796  ntrneineine1lem  39797  ntrneiel2  39799  cpcolld  39969  expandrexn  40002  ismnuprim  40005  rr-grothprimbi  40006  rr-groth  40010  rexbidar  40197  onfrALTlem5  40295  onfrALTlem2  40299  onfrALTlem1  40301  onfrALTlem5VD  40638  onfrALTlem2VD  40642  onfrALTlem1VD  40643  chordthmALT  40686  rspcegf  40699  cncmpmax  40708  rfcnnnub  40712  inn0f  40755  nssrex  40771  eluni2f  40793  eliin2f  40794  suprnmpt  40855  founiiun0  40876  disjinfi  40879  fvelima2  40961  ssfiunibd  41006  infrpge  41049  fsumiunss  41288  islpcn  41352  lptre2pt  41353  stoweidlem14  41731  stoweidlem34  41751  stoweidlem35  41752  stoweidlem43  41760  stoweidlem44  41761  stoweidlem50  41767  stoweidlem54  41771  stoweidlem56  41773  stoweidlem59  41776  stoweidlem60  41777  fourier2  41944  qndenserrnbllem  42011  qndenserrn  42016  sge0rpcpnf  42135  hoidmvval0b  42304  hoiqssbllem3  42338  nfermltl8rev  43276  nfermltl2rev  43277  nfermltlrev  43278  opeliun2xp  43746  setrec1lem3  44160