Definition df-rex 3063

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 3053). (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 3062	. 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  3064  rexex  3068  rextru  3069  reximi2  3071  rexbii2  3081  rexlimiva  3131  reximdv2  3148  rexbidv2  3158  r19.41v  3168  r3ex  3177  reeanlem  3209  risset  3213  cbvrexvw  3217  rspe  3228  r19.23t  3234  r19.41  3242  reximd2a  3248  rexbida  3250  nfre1  3263  rexcom4  3265  r19.12  3287  rexeq  3292  reu5  3345  rmo5  3361  rexv  3458  2gencl  3473  3gencl  3474  rspce  3554  ceqsrexv  3598  rexab2  3646  rexrab2  3647  morex  3666  reu2  3672  reu6  3673  reu3  3674  2reuswap  3693  2reuswap2  3694  2reu5lem3  3704  2reu5  3705  2rmoswap  3708  ssrexf  3989  ssrexv  3992  rexss  3998  rexdifi  4091  rexun  4137  reuun2  4266  reuss2  4267  reupick  4270  reupick3  4271  euelss  4273  reximdva0  4296  n0rex  4298  n0el  4305  inn0f  4312  r19.2z  4440  rexsns  4616  exsnrex  4625  dfuni2  4853  eluni2  4855  elunirab  4866  iuncom4  4943  iunxiun  5040  axrep6  5222  axrep6OLD  5223  replem  5224  axsepgfromrep  5230  intexrab  5287  opeliunxp  5695  opeliun2xp  5696  xpiundi  5699  xpiundir  5700  ssrelrn  5847  dmuni  5867  rnmpt  5910  elrnmpt1  5913  dfima2  6025  dfima3  6026  elima2  6029  dfco2a  6208  imaco  6213  elsnxp  6253  dfpo2  6258  fvelima2  6890  dffo4  7053  dffo5  7054  abrexco  7196  isomin  7289  imaeqsexvOLD  7315  imaeqexov  7602  zfrep6OLD  7905  opabex3d  7915  opabex3rd  7916  opabex3  7917  abexssex  7920  abexex  7921  frxp  8073  dfrecs3  8309  rdglim2  8368  oarec  8494  oeeu  8536  mapsnd  8831  mapsnend  8980  pssnn  9100  enfii  9117  enp1i  9186  unblem2  9200  pwfir  9224  dffi2  9333  marypha2lem4  9348  marypha2  9349  zfregcl  9506  zfregclOLD  9507  axinf2  9558  zfinf2  9560  brttrcl2  9632  ttrclselem2  9644  rankuni  9784  scott0  9807  cp  9812  bnd2  9814  infpwfien  9981  aceq1  10036  dfac5lem2  10043  dfac5lem3  10044  dfac2b  10050  kmlem3  10072  kmlem6  10075  kmlem8  10077  kmlem14  10083  infmap2  10136  ackbij2  10161  cfub  10168  cfval2  10179  cflim3  10181  cfss  10184  cfslb  10185  isf32lem9  10280  zorn2lem6  10420  iundom2g  10459  winalim2  10616  grothprim  10754  genpass  10929  nqpr  10934  1idpr  10949  ltexprlem4  10959  ltexprlem5  10960  reclem2pr  10968  axrrecex  11083  dedekind  11306  sup2  12109  infm3  12112  nnunb  12430  2rexuz  12847  nnwos  12862  xrsupsslem  13256  xrinfmsslem  13257  hashgt23el  14383  ishashinf  14422  wwlktovfo  14917  maxprmfct  16676  vdwapun  16942  vdwmc  16946  vdwmc2  16947  ram0  16990  imasleval  17502  mreexexlem2d  17608  dfiso2  17736  isssc  17784  drsdirfi  18268  dirge  18566  pwmnd  18905  psgnunilem4  19469  odcau  19576  ablfac2  20063  lspprat  21148  lidlnz  21237  isbasis2g  22910  tgval2  22918  ntreq0  23039  neitr  23142  cmpfi  23370  is1stc2  23404  2ndcsb  23411  2ndcsep  23421  1stcelcls  23423  hausmapdom  23462  isfbas2  23797  fbssint  23800  isfil2  23818  elfg  23833  fgcl  23840  uffix2  23886  alexsubALTlem4  24012  lpbl  24465  metustexhalf  24518  metuel2  24527  restmetu  24532  bcthlem5  25292  lrrecfr  27932  upgrex  29158  uvtx01vtx  29463  uhgrvd00  29600  wlkswwlksf1o  29944  wwlksnextsurj  29965  frcond3  30336  frgr3vlem2  30341  3vfriswmgrlem  30344  frgrncvvdeqlem9  30374  ubthlem1  30938  axhcompl-zf  31066  isch3  31309  shne0i  31516  cnlnssadj  32148  reuxfrdf  32557  rexunirn  32558  rmoxfrd  32559  dmrab  32563  abrexdomjm  32574  abrexexd  32576  iunrnmptss  32632  ac6mapd  32693  1stpreimas  32776  fpwrelmapffslem  32802  qsxpid  33419  krull  33536  zarclsint  34013  ordtconnlem1  34065  ddemeas  34377  omssubaddlem  34440  omssubadd  34441  eulerpartlemgvv  34517  tgoldbachgt  34804  bnj168  34870  bnj956  34916  bnj1098  34923  bnj1143  34929  bnj1146  34930  bnj1185  34932  bnj1196  34933  bnj600  35058  bnj849  35064  bnj906  35069  bnj916  35072  bnj983  35090  bnj984  35091  bnj1083  35117  bnj1176  35144  bnj1186  35146  bnj1189  35148  bnj1228  35150  bnj1253  35156  bnj1398  35173  bnj1463  35194  bnj1312  35197  bnj1514  35202  exdifsn  35218  r1filimi  35243  axprALT2  35250  axregszf  35270  onvf1odlem1  35282  onvf1odlem2  35283  wevgblacfn  35288  lfuhgr3  35299  cusgredgex  35301  loop1cycl  35316  erdszelem10  35379  ptpconn  35412  rexxfr3dALT  35818  coep  35931  coepr  35932  dffr5  35933  opelco3  35954  dfon2lem8  35967  brimg  36114  dfrecs2  36129  dfrdg4  36130  ellines  36331  cbvrexvw2  36406  neifg  36550  regsfromunir1  36719  bj-rexvw  37184  bj-gabima  37244  bj-snglc  37273  bj-snglss  37274  bj-axseprep  37378  bj-axreprepsep  37379  bj-rest10  37397  bj-restn0  37399  bj-restpw  37401  bj-rest0  37402  bj-restb  37403  bj-restuni  37406  bj-dfmpoa  37427  bj-finsumval0  37596  rnmptsn  37648  f1omptsnlem  37649  mptsnunlem  37651  topdifinffinlem  37660  isbasisrelowllem1  37668  isbasisrelowllem2  37669  relowlpssretop  37677  fvineqsneq  37725  pibt2  37730  poimirlem30  37968  abrexdom  38048  prdstotbnd  38112  elrnres  38596  eldmqsres2  38612  exanres  38619  rncnvepres  38627  rnxrnres  38740  1cossres  38837  eldm1cossres  38868  eldmqs1cossres  39062  disjlem17  39220  disjdmqscossss  39224  prtlem17  39319  prter2  39324  islshpat  39460  lsat0cv  39476  lshpsmreu  39552  atex  39849  islpln5  39978  islvol5  40022  pmapglb  40213  pmapglb2N  40214  pmapglb2xN  40215  elpaddn0  40243  pmapjat1  40296  polval2N  40349  osumcllem11N  40409  pexmidlem8N  40420  cdlemftr3  41008  dibelval3  41590  dibglbN  41609  dicelval3  41623  dihglbcpreN  41743  dihglb2  41785  dihjatcclem4  41864  mapdrvallem2  42088  mapdpglem3  42118  hdmapglem7a  42370  sticksstones3  42584  imaopab  42669  sn-sup2  42933  fimgmcyc  42976  prjspeclsp  43042  uniel  43642  nnoeomeqom  43737  tfsconcatlem  43761  tfsconcatrn  43767  tfsconcat0i  43770  rp-isfinite5  43941  rp-isfinite6  43942  minregex  43958  elintima  44077  iunrelexpuztr  44143  cotrclrcl  44166  neik0pk1imk0  44471  ntrneineine0lem  44507  ntrneineine1lem  44508  ntrneiel2  44510  cpcolld  44682  expandrexn  44715  ismnuprim  44718  rr-grothprimbi  44719  rr-groth  44723  ismnushort  44725  rr-grothshortbi  44727  rexbidar  44869  onfrALTlem5  44966  onfrALTlem2  44970  onfrALTlem1  44972  onfrALTlem5VD  45308  onfrALTlem2VD  45312  onfrALTlem1VD  45313  chordthmALT  45356  rspesbcd  45361  modelaxreplem3  45404  ssclaxsep  45406  permaxrep  45430  nregmodel  45441  rspcegf  45451  cncmpmax  45460  rfcnnnub  45464  nssrex  45513  eluni2f  45530  eliin2f  45531  suprnmpt  45601  founiiun0  45617  disjinfi  45619  ssfiunibd  45739  infrpge  45778  fsumiunss  46002  islpcn  46064  lptre2pt  46065  stoweidlem14  46439  stoweidlem34  46459  stoweidlem35  46460  stoweidlem43  46468  stoweidlem44  46469  stoweidlem50  46475  stoweidlem54  46479  stoweidlem56  46481  stoweidlem59  46484  stoweidlem60  46485  fourier2  46652  qndenserrnbllem  46719  qndenserrn  46724  sge0rpcpnf  46846  hoidmvval0b  47015  hoiqssbllem3  47049  chnsubseqword  47303  imasetpreimafvbijlemfv1  47854  nfermltl8rev  48209  nfermltl2rev  48210  nfermltlrev  48211  isubgredg  48333  gpg5edgnedg  48597  nn0mnd  48646  opncldeqv  49368  opnneilv  49375  setrec1lem3  50155