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 1568	. . . . 5 class 𝑥
6	5, 3	wcel 2144	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 401	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wex 1811	. 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  3608  rexab2  3656  rexrab2  3657  morex  3676  reu2  3682  reu6  3683  reu3  3684  2reuswap  3703  2reuswap2  3704  2reu5lem3  3714  2reu5  3715  2rmoswap  3718  nssrex  3973  ssrexf  3975  ssrexv  3978  rexss  3982  rexdifi  4086  rexun  4194  reuun2  4270  reuss2  4271  reupick  4274  reupick3  4275  euelss  4277  reximdva0  4302  n0rex  4304  n0el  4311  inn0f  4318  r19.2z  4454  rexsns  4631  exsnrex  4640  dfuni2  4868  eluni2  4870  elunirab  4881  iuncom4  4959  iunxiun  5056  axrep6  5239  replem  5240  axsepgfromrep  5246  intexrab  5307  opeliunxp  5717  opeliun2xp  5718  xpiundi  5721  xpiundir  5722  ssrelrn  5875  dmuni  5895  rnmpt  5938  elrnmpt1  5941  dfima2  6057  dfima3  6058  elima2  6061  dfco2a  6247  imaco  6252  elsnxp  6294  dfpo2  6299  fvelima2  6937  dffo4  7103  dffo5  7104  abrexco  7248  isomin  7345  imaeqexov  7659  zfrep6OLD  7967  opabex3d  7977  opabex3rd  7978  opabex3  7979  abexssex  7982  abexex  7983  frxp  8138  dfrecs3  8380  rdglim2  8440  oarec  8570  oeeu  8612  mapsnd  8914  mapsnend  9064  pssnn  9184  enfii  9201  enp1i  9270  unblem2  9285  pwfir  9308  dffi2  9415  marypha2lem4  9430  marypha2  9431  zfregcl  9588  zfregclOLD  9589  axinf2  9641  zfinf2  9643  brttrcl2  9715  ttrclselem2  9727  rankuni  9879  r1filimi  9903  scott0b  9937  scott0OLD  9938  cp  9954  bnd2  9956  setrec1lem3  9969  infpwfien  10141  aceq1  10196  dfac5lem2  10203  dfac5lem3  10204  dfac2b  10209  kmlem3  10231  kmlem6  10234  kmlem8  10236  kmlem14  10242  infmap2  10295  ackbij2  10320  cfub  10326  cfval2  10338  cflim3  10340  cfss  10343  cfslb  10344  isf32lem9  10439  zorn2lem6  10579  iundom2g  10624  winalim2  10781  grothprim  10919  genpass  11094  nqpr  11099  1idpr  11114  ltexprlem4  11124  ltexprlem5  11125  reclem2pr  11133  axrrecex  11248  dedekind  11473  sup2  12273  infm3  12276  nnunb  12602  2rexuz  13027  nnwos  13042  xrsupsslem  13437  xrinfmsslem  13438  hashgt23el  14569  ishashinf  14608  wwlktovfo  15111  maxprmfct  16885  vdwapun  17152  vdwmc  17156  vdwmc2  17157  ram0  17200  imasleval  17713  mreexexlem2d  17819  dfiso2  17947  isssc  17995  drsdirfi  18479  dirge  18777  pwmnd  19143  qsxpid  19387  psgnunilem4  19711  odcau  19818  ablfac2  20305  lspprat  21431  lidlnz  21530  isbasis2g  23266  tgval2  23274  ntreq0  23395  neitr  23498  cmpfi  23726  is1stc2  23760  2ndcsb  23767  2ndcsep  23778  1stcelcls  23780  hausmapdom  23819  isfbas2  24154  fbssint  24157  isfil2  24175  elfg  24190  fgcl  24197  uffix2  24243  alexsubALTlem4  24369  lpbl  24822  metustexhalf  24875  metuel2  24884  restmetu  24889  bcthlem5  25649  lrrecfr  28329  upgrex  29670  lfuhgr3  29728  uvtx01vtx  29978  uhgrvd00  30115  wlkswwlksf1o  30468  wwlksnextsurj  30489  loop1cycl  30744  frcond3  30870  frgr3vlem2  30875  3vfriswmgrlem  30878  frgrncvvdeqlem9  30908  ubthlem1  31472  axhcompl-zf  31600  isch3  31843  shne0i  32050  cnlnssadj  32682  reuxfrdf  33129  rexunirn  33130  rmoxfrd  33131  dmrab  33135  abrexdomjm  33145  abrexexd  33147  iunrnmptss  33201  ac6mapd  33259  1stpreimas  33341  fpwrelmapffslem  33366  krull  34045  zarclsint  34546  ordtconnlem1  34598  ddemeas  34911  omssubaddlem  34973  omssubadd  34974  eulerpartlemgvv  35050  tgoldbachgt  35334  bnj168  35403  bnj956  35449  bnj1098  35456  bnj1143  35462  bnj1146  35463  bnj1185  35465  bnj1196  35466  bnj600  35591  bnj849  35597  bnj906  35602  bnj916  35605  bnj983  35623  bnj984  35624  bnj1083  35650  bnj1176  35677  bnj1186  35679  bnj1189  35681  bnj1228  35683  bnj1253  35689  bnj1398  35706  bnj1463  35727  bnj1312  35730  bnj1514  35735  exdifsn  35753  axprALT2  35776  axregszf  35839  karddom  35871  kardsdom  35872  kardfi  35880  onvf1odlem1  35924  onvf1odlem2  35925  wevgblacfn  35932  cusgredgex  35948  erdszelem10  36007  ptpconn  36040  rexxfr3dALT  36446  coep  36559  coepr  36560  dffr5  36561  opelco3  36581  dfon2lem8  36594  brimg  36741  dfrecs2  36756  dfrdg4  36757  ellines  36959  cbvrexvw2  37058  neifg  37201  regsfromunir1  37370  bj-rexvw  37834  bj-gabima  37895  bj-snglc  37924  bj-snglss  37925  bj-axseprep  38032  bj-axreprepsep  38033  bj-rest10  38051  bj-restn0  38053  bj-restpw  38055  bj-rest0  38056  bj-restb  38057  bj-restuni  38060  bj-dfmpoa  38082  bj-finsumval0  38249  rnmptsn  38301  f1omptsnlem  38302  mptsnunlem  38304  topdifinffinlem  38313  isbasisrelowllem1  38321  isbasisrelowllem2  38322  relowlpssretop  38330  fvineqsneq  38378  pibt2  38383  poimirlem30  38611  negprop  38686  impprop  38687  dfprop1  38688  abrexdom  38707  prdstotbnd  38771  elrnres  39253  eldmqsres2  39269  exanres  39276  rncnvepres  39284  rnxrnres  39397  1cossres  39494  eldm1cossres  39525  eldmqs1cossres  39719  disjlem17  39877  disjdmqscossss  39881  prtlem17  39976  prter2  39981  islshpat  40117  lsat0cv  40133  lshpsmreu  40209  atex  40506  islpln5  40635  islvol5  40679  pmapglb  40870  pmapglb2N  40871  pmapglb2xN  40872  elpaddn0  40900  pmapjat1  40953  polval2N  41006  osumcllem11N  41066  pexmidlem8N  41077  cdlemftr3  41665  dibelval3  42247  dibglbN  42266  dicelval3  42280  dihglbcpreN  42400  dihglb2  42442  dihjatcclem4  42521  mapdrvallem2  42745  mapdpglem3  42775  hdmapglem7a  43027  sticksstones3  43241  imaopab  43328  sn-sup2  43598  fimgmcyc  43641  prjspeclsp  43683  uniel  44261  nnoeomeqom  44356  tfsconcatlem  44380  tfsconcatrn  44386  tfsconcat0i  44389  rp-isfinite5  44560  rp-isfinite6  44561  minregex  44577  elintima  44695  iunrelexpuztr  44761  cotrclrcl  44784  neik0pk1imk0  45089  ntrneineine0lem  45125  ntrneineine1lem  45126  ntrneiel2  45128  cpcolld  45284  expandrexn  45317  ismnuprim  45320  rr-grothprimbi  45321  rr-groth  45325  ismnushort  45327  rr-grothshortbi  45329  rexbidar  45471  onfrALTlem5  45567  onfrALTlem2  45571  onfrALTlem1  45573  onfrALTlem5VD  45909  onfrALTlem2VD  45913  onfrALTlem1VD  45914  chordthmALT  45957  rspesbcd  45962  modelaxreplem3  46012  ssclaxsep  46014  permaxrep  46038  nregmodel  46049  rspcegf  46082  cncmpmax  46091  rfcnnnub  46095  eluni2f  46160  eliin2f  46161  suprnmpt  46231  founiiun0  46247  disjinfi  46249  ssfiunibd  46367  infrpge  46405  fsumiunss  46629  islpcn  46691  lptre2pt  46692  stoweidlem14  47066  stoweidlem34  47086  stoweidlem35  47087  stoweidlem43  47095  stoweidlem44  47096  stoweidlem50  47102  stoweidlem54  47106  stoweidlem56  47108  stoweidlem59  47111  stoweidlem60  47112  fourier2  47279  qndenserrnbllem  47346  qndenserrn  47351  sge0rpcpnf  47473  hoidmvval0b  47642  hoiqssbllem3  47676  tmachlem-exagreecover  47998  imasetpreimafvbijlemfv1  48527  nfermltl8rev  48882  nfermltl2rev  48883  nfermltlrev  48884  isubgredg  49006  gpg5edgnedg  49270  nn0mnd  49318  opncldbid  50052  opnneilv  50059  dfrals2  50928