Definition df-rex 3060

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

This definition is referenced by:  ralnex  3061  rexex  3065  rextru  3066  reximi2  3068  rexbii2  3078  rexlimiva  3128  reximdv2  3145  rexbidv2  3155  r19.41v  3165  r3ex  3174  reeanlem  3206  risset  3210  cbvrexvw  3214  rspe  3225  r19.23t  3231  r19.41  3239  reximd2a  3245  rexbida  3247  nfre1  3260  rexcom4  3262  r19.12  3284  rexeq  3289  reu5  3342  rmo5  3358  rexv  3455  2gencl  3470  3gencl  3471  rspce  3551  ceqsrexv  3595  rexab2  3642  rexrab2  3643  morex  3662  reu2  3668  reu6  3669  reu3  3670  2reuswap  3689  2reuswap2  3690  2reu5lem3  3700  2reu5  3701  2rmoswap  3704  ssrexf  3983  ssrexv  3986  rexss  3990  rexdifi  4082  rexun  4127  reuun2  4255  reuss2  4256  reupick  4259  reupick3  4260  euelss  4262  reximdva0  4285  n0rex  4287  n0el  4294  inn0f  4301  r19.2z  4429  rexsns  4605  exsnrex  4614  dfuni2  4842  eluni2  4844  elunirab  4855  iuncom4  4932  iunxiun  5028  axrep6  5210  axrep6OLD  5211  replem  5212  axsepgfromrep  5218  intexrab  5277  opeliunxp  5687  opeliun2xp  5688  xpiundi  5691  xpiundir  5692  ssrelrn  5838  dmuni  5858  rnmpt  5901  elrnmpt1  5904  dfima2  6016  dfima3  6017  elima2  6020  dfco2a  6199  imaco  6204  elsnxp  6244  dfpo2  6249  fvelima2  6881  dffo4  7044  dffo5  7045  abrexco  7188  isomin  7281  imaeqsexvOLD  7307  imaeqexov  7594  zfrep6OLD  7897  opabex3d  7907  opabex3rd  7908  opabex3  7909  abexssex  7912  abexex  7913  frxp  8065  dfrecs3  8301  rdglim2  8360  oarec  8486  oeeu  8528  mapsnd  8823  mapsnend  8972  pssnn  9092  enfii  9109  enp1i  9178  unblem2  9192  pwfir  9216  dffi2  9325  marypha2lem4  9340  marypha2  9341  zfregcl  9498  zfregclOLD  9499  axinf2  9550  zfinf2  9552  brttrcl2  9624  ttrclselem2  9636  rankuni  9776  scott0  9799  cp  9804  bnd2  9806  infpwfien  9973  aceq1  10028  dfac5lem2  10035  dfac5lem3  10036  dfac2b  10042  kmlem3  10064  kmlem6  10067  kmlem8  10069  kmlem14  10075  infmap2  10128  ackbij2  10153  cfub  10160  cfval2  10171  cflim3  10173  cfss  10176  cfslb  10177  isf32lem9  10272  zorn2lem6  10412  iundom2g  10451  winalim2  10608  grothprim  10746  genpass  10921  nqpr  10926  1idpr  10941  ltexprlem4  10951  ltexprlem5  10952  reclem2pr  10960  axrrecex  11075  dedekind  11298  sup2  12101  infm3  12104  nnunb  12422  2rexuz  12839  nnwos  12854  xrsupsslem  13248  xrinfmsslem  13249  hashgt23el  14375  ishashinf  14414  wwlktovfo  14909  maxprmfct  16668  vdwapun  16934  vdwmc  16938  vdwmc2  16939  ram0  16982  imasleval  17494  mreexexlem2d  17600  dfiso2  17728  isssc  17776  drsdirfi  18260  dirge  18558  pwmnd  18897  psgnunilem4  19461  odcau  19568  ablfac2  20055  lspprat  21140  lidlnz  21229  isbasis2g  22901  tgval2  22909  ntreq0  23030  neitr  23133  cmpfi  23361  is1stc2  23395  2ndcsb  23402  2ndcsep  23412  1stcelcls  23414  hausmapdom  23453  isfbas2  23788  fbssint  23791  isfil2  23809  elfg  23824  fgcl  23831  uffix2  23877  alexsubALTlem4  24003  lpbl  24456  metustexhalf  24509  metuel2  24518  restmetu  24523  bcthlem5  25283  lrrecfr  27923  upgrex  29149  uvtx01vtx  29454  uhgrvd00  29591  wlkswwlksf1o  29935  wwlksnextsurj  29956  frcond3  30327  frgr3vlem2  30332  3vfriswmgrlem  30335  frgrncvvdeqlem9  30365  ubthlem1  30929  axhcompl-zf  31057  isch3  31300  shne0i  31507  cnlnssadj  32139  reuxfrdf  32548  rexunirn  32549  rmoxfrd  32550  dmrab  32554  abrexdomjm  32565  abrexexd  32567  iunrnmptss  32623  ac6mapd  32684  1stpreimas  32767  fpwrelmapffslem  32793  qsxpid  33410  krull  33527  zarclsint  34004  ordtconnlem1  34056  ddemeas  34368  omssubaddlem  34431  omssubadd  34432  eulerpartlemgvv  34508  tgoldbachgt  34795  bnj168  34861  bnj956  34907  bnj1098  34914  bnj1143  34920  bnj1146  34921  bnj1185  34923  bnj1196  34924  bnj600  35049  bnj849  35055  bnj906  35060  bnj916  35063  bnj983  35081  bnj984  35082  bnj1083  35108  bnj1176  35135  bnj1186  35137  bnj1189  35139  bnj1228  35141  bnj1253  35147  bnj1398  35164  bnj1463  35185  bnj1312  35188  bnj1514  35193  exdifsn  35209  r1filimi  35234  axprALT2  35241  axregszf  35261  onvf1odlem1  35273  onvf1odlem2  35274  wevgblacfn  35279  lfuhgr3  35290  cusgredgex  35292  loop1cycl  35307  erdszelem10  35370  ptpconn  35403  rexxfr3dALT  35809  coep  35922  coepr  35923  dffr5  35924  opelco3  35945  dfon2lem8  35958  brimg  36105  dfrecs2  36120  dfrdg4  36121  ellines  36322  cbvrexvw2  36397  neifg  36541  regsfromunir1  36710  bj-rexvw  37175  bj-gabima  37235  bj-snglc  37264  bj-snglss  37265  bj-axseprep  37369  bj-axreprepsep  37370  bj-rest10  37388  bj-restn0  37390  bj-restpw  37392  bj-rest0  37393  bj-restb  37394  bj-restuni  37397  bj-dfmpoa  37418  bj-finsumval0  37587  rnmptsn  37639  f1omptsnlem  37640  mptsnunlem  37642  topdifinffinlem  37651  isbasisrelowllem1  37659  isbasisrelowllem2  37660  relowlpssretop  37668  fvineqsneq  37716  pibt2  37721  poimirlem30  37959  abrexdom  38039  prdstotbnd  38103  elrnres  38587  eldmqsres2  38603  exanres  38610  rncnvepres  38618  rnxrnres  38731  1cossres  38828  eldm1cossres  38859  eldmqs1cossres  39053  disjlem17  39211  disjdmqscossss  39215  prtlem17  39310  prter2  39315  islshpat  39451  lsat0cv  39467  lshpsmreu  39543  atex  39840  islpln5  39969  islvol5  40013  pmapglb  40204  pmapglb2N  40205  pmapglb2xN  40206  elpaddn0  40234  pmapjat1  40287  polval2N  40340  osumcllem11N  40400  pexmidlem8N  40411  cdlemftr3  40999  dibelval3  41581  dibglbN  41600  dicelval3  41614  dihglbcpreN  41734  dihglb2  41776  dihjatcclem4  41855  mapdrvallem2  42079  mapdpglem3  42109  hdmapglem7a  42361  sticksstones3  42575  imaopab  42660  sn-sup2  42924  fimgmcyc  42967  prjspeclsp  43033  uniel  43633  nnoeomeqom  43728  tfsconcatlem  43752  tfsconcatrn  43758  tfsconcat0i  43761  rp-isfinite5  43932  rp-isfinite6  43933  minregex  43949  elintima  44068  iunrelexpuztr  44134  cotrclrcl  44157  neik0pk1imk0  44462  ntrneineine0lem  44498  ntrneineine1lem  44499  ntrneiel2  44501  cpcolld  44673  expandrexn  44706  ismnuprim  44709  rr-grothprimbi  44710  rr-groth  44714  ismnushort  44716  rr-grothshortbi  44718  rexbidar  44860  onfrALTlem5  44957  onfrALTlem2  44961  onfrALTlem1  44963  onfrALTlem5VD  45299  onfrALTlem2VD  45303  onfrALTlem1VD  45304  chordthmALT  45347  rspesbcd  45352  modelaxreplem3  45395  ssclaxsep  45397  permaxrep  45421  nregmodel  45432  rspcegf  45442  cncmpmax  45451  rfcnnnub  45455  nssrex  45504  eluni2f  45521  eliin2f  45522  suprnmpt  45592  founiiun0  45608  disjinfi  45610  ssfiunibd  45730  infrpge  45769  fsumiunss  45993  islpcn  46055  lptre2pt  46056  stoweidlem14  46430  stoweidlem34  46450  stoweidlem35  46451  stoweidlem43  46459  stoweidlem44  46460  stoweidlem50  46466  stoweidlem54  46470  stoweidlem56  46472  stoweidlem59  46475  stoweidlem60  46476  fourier2  46643  qndenserrnbllem  46710  qndenserrn  46715  sge0rpcpnf  46837  hoidmvval0b  47006  hoiqssbllem3  47040  chnsubseqword  47296  imasetpreimafvbijlemfv1  47851  nfermltl8rev  48206  nfermltl2rev  48207  nfermltlrev  48208  isubgredg  48330  gpg5edgnedg  48594  nn0mnd  48643  opncldeqv  49365  opnneilv  49372  setrec1lem3  50152