Definition df-rex 3066

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 3056). (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 3065	. 2 wff ∃𝑥 ∈ 𝐴 𝜑
5	2	cv 1547	. . . . 5 class 𝑥
6	5, 3	wcel 2121	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 397	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wex 1787	. 2 wff ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 208	1 wff (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  ralnex  3067  rexex  3071  rextru  3072  reximi2  3074  rexbii2  3084  rexlimiva  3134  reximdv2  3151  rexbidv2  3161  r19.41v  3171  r3ex  3180  reeanlem  3212  risset  3216  cbvrexvw  3220  rspe  3231  r19.23t  3237  r19.41  3245  reximd2a  3251  rexbida  3253  nfre1  3266  rexcom4  3268  r19.12  3290  rexeq  3295  reu5  3348  rmo5  3364  rexv  3460  2gencl  3475  3gencl  3476  rspce  3550  ceqsrexv  3594  rexab2  3641  rexrab2  3642  morex  3661  reu2  3667  reu6  3668  reu3  3669  2reuswap  3688  2reuswap2  3689  2reu5lem3  3699  2reu5  3700  2rmoswap  3703  nssrex  3981  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  5842  dmuni  5862  rnmpt  5905  elrnmpt1  5908  dfima2  6020  dfima3  6021  elima2  6024  dfco2a  6200  imaco  6205  elsnxp  6245  dfpo2  6250  fvelima2  6882  dffo4  7047  dffo5  7048  abrexco  7191  isomin  7284  imaeqsexvOLD  7310  imaeqexov  7597  zfrep6OLD  7899  opabex3d  7909  opabex3rd  7910  opabex3  7911  abexssex  7914  abexex  7915  frxp  8068  dfrecs3  8305  rdglim2  8365  oarec  8491  oeeu  8533  mapsnd  8828  mapsnend  8977  pssnn  9097  enfii  9114  enp1i  9183  unblem2  9197  pwfir  9221  dffi2  9330  marypha2lem4  9345  marypha2  9346  zfregcl  9503  zfregclOLD  9504  axinf2  9556  zfinf2  9558  brttrcl2  9630  ttrclselem2  9642  rankuni  9782  scott0  9805  cp  9810  bnd2  9812  infpwfien  9979  aceq1  10034  dfac5lem2  10041  dfac5lem3  10042  dfac2b  10048  kmlem3  10070  kmlem6  10073  kmlem8  10075  kmlem14  10081  infmap2  10134  ackbij2  10159  cfub  10166  cfval2  10178  cflim3  10180  cfss  10183  cfslb  10184  isf32lem9  10279  zorn2lem6  10419  iundom2g  10458  winalim2  10615  grothprim  10753  genpass  10928  nqpr  10933  1idpr  10948  ltexprlem4  10958  ltexprlem5  10959  reclem2pr  10967  axrrecex  11082  dedekind  11305  sup2  12107  infm3  12110  nnunb  12428  2rexuz  12845  nnwos  12860  xrsupsslem  13254  xrinfmsslem  13255  hashgt23el  14381  ishashinf  14420  wwlktovfo  14915  maxprmfct  16674  vdwapun  16940  vdwmc  16944  vdwmc2  16945  ram0  16988  imasleval  17500  mreexexlem2d  17606  dfiso2  17734  isssc  17782  drsdirfi  18266  dirge  18564  pwmnd  18903  psgnunilem4  19466  odcau  19573  ablfac2  20060  lspprat  21149  lidlnz  21238  isbasis2g  22934  tgval2  22942  ntreq0  23063  neitr  23166  cmpfi  23394  is1stc2  23428  2ndcsb  23435  2ndcsep  23445  1stcelcls  23447  hausmapdom  23486  isfbas2  23821  fbssint  23824  isfil2  23842  elfg  23857  fgcl  23864  uffix2  23910  alexsubALTlem4  24036  lpbl  24489  metustexhalf  24542  metuel2  24551  restmetu  24556  bcthlem5  25316  lrrecfr  27955  upgrex  29181  uvtx01vtx  29486  uhgrvd00  29623  wlkswwlksf1o  29967  wwlksnextsurj  29988  frcond3  30359  frgr3vlem2  30364  3vfriswmgrlem  30367  frgrncvvdeqlem9  30397  ubthlem1  30961  axhcompl-zf  31089  isch3  31332  shne0i  31539  cnlnssadj  32171  reuxfrdf  32580  rexunirn  32581  rmoxfrd  32582  dmrab  32586  abrexdomjm  32597  abrexexd  32599  iunrnmptss  32656  ac6mapd  32717  1stpreimas  32800  fpwrelmapffslem  32826  qsxpid  33447  krull  33564  zarclsint  34066  ordtconnlem1  34118  ddemeas  34430  omssubaddlem  34493  omssubadd  34494  eulerpartlemgvv  34570  tgoldbachgt  34857  bnj168  34926  bnj956  34972  bnj1098  34979  bnj1143  34985  bnj1146  34986  bnj1185  34988  bnj1196  34989  bnj600  35114  bnj849  35120  bnj906  35125  bnj916  35128  bnj983  35146  bnj984  35147  bnj1083  35173  bnj1176  35200  bnj1186  35202  bnj1189  35204  bnj1228  35206  bnj1253  35212  bnj1398  35229  bnj1463  35250  bnj1312  35253  bnj1514  35258  exdifsn  35274  r1filimi  35297  axprALT2  35303  axregszf  35323  onvf1odlem1  35344  onvf1odlem2  35345  wevgblacfn  35350  lfuhgr3  35361  cusgredgex  35363  loop1cycl  35378  erdszelem10  35441  ptpconn  35474  rexxfr3dALT  35880  coep  35993  coepr  35994  dffr5  35995  opelco3  36016  dfon2lem8  36029  brimg  36176  dfrecs2  36191  dfrdg4  36192  ellines  36393  cbvrexvw2  36468  neifg  36612  regsfromunir1  36781  bj-rexvw  37246  bj-gabima  37306  bj-snglc  37335  bj-snglss  37336  bj-axseprep  37440  bj-axreprepsep  37441  bj-rest10  37459  bj-restn0  37461  bj-restpw  37463  bj-rest0  37464  bj-restb  37465  bj-restuni  37468  bj-dfmpoa  37489  bj-finsumval0  37658  rnmptsn  37710  f1omptsnlem  37711  mptsnunlem  37713  topdifinffinlem  37722  isbasisrelowllem1  37730  isbasisrelowllem2  37731  relowlpssretop  37739  fvineqsneq  37787  pibt2  37792  poimirlem30  38030  abrexdom  38110  prdstotbnd  38174  elrnres  38658  eldmqsres2  38674  exanres  38681  rncnvepres  38689  rnxrnres  38802  1cossres  38899  eldm1cossres  38930  eldmqs1cossres  39124  disjlem17  39282  disjdmqscossss  39286  prtlem17  39381  prter2  39386  islshpat  39522  lsat0cv  39538  lshpsmreu  39614  atex  39911  islpln5  40040  islvol5  40084  pmapglb  40275  pmapglb2N  40276  pmapglb2xN  40277  elpaddn0  40305  pmapjat1  40358  polval2N  40411  osumcllem11N  40471  pexmidlem8N  40482  cdlemftr3  41070  dibelval3  41652  dibglbN  41671  dicelval3  41685  dihglbcpreN  41805  dihglb2  41847  dihjatcclem4  41926  mapdrvallem2  42150  mapdpglem3  42180  hdmapglem7a  42432  sticksstones3  42646  imaopab  42731  sn-sup2  42994  fimgmcyc  43033  prjspeclsp  43075  uniel  43675  nnoeomeqom  43770  tfsconcatlem  43794  tfsconcatrn  43800  tfsconcat0i  43803  rp-isfinite5  43974  rp-isfinite6  43975  minregex  43991  elintima  44110  iunrelexpuztr  44176  cotrclrcl  44199  neik0pk1imk0  44504  ntrneineine0lem  44540  ntrneineine1lem  44541  ntrneiel2  44543  cpcolld  44715  expandrexn  44748  ismnuprim  44751  rr-grothprimbi  44752  rr-groth  44756  ismnushort  44758  rr-grothshortbi  44760  rexbidar  44902  onfrALTlem5  44999  onfrALTlem2  45003  onfrALTlem1  45005  onfrALTlem5VD  45341  onfrALTlem2VD  45345  onfrALTlem1VD  45346  chordthmALT  45389  rspesbcd  45394  modelaxreplem3  45437  ssclaxsep  45439  permaxrep  45463  nregmodel  45474  rspcegf  45484  cncmpmax  45493  rfcnnnub  45497  eluni2f  45562  eliin2f  45563  suprnmpt  45633  founiiun0  45649  disjinfi  45651  ssfiunibd  45769  infrpge  45808  fsumiunss  46032  islpcn  46094  lptre2pt  46095  stoweidlem14  46469  stoweidlem34  46489  stoweidlem35  46490  stoweidlem43  46498  stoweidlem44  46499  stoweidlem50  46505  stoweidlem54  46509  stoweidlem56  46511  stoweidlem59  46514  stoweidlem60  46515  fourier2  46682  qndenserrnbllem  46749  qndenserrn  46754  sge0rpcpnf  46876  hoidmvval0b  47045  hoiqssbllem3  47079  chnsubseqword  47335  imasetpreimafvbijlemfv1  47890  nfermltl8rev  48245  nfermltl2rev  48246  nfermltlrev  48247  isubgredg  48369  gpg5edgnedg  48633  nn0mnd  48682  opncldeqv  49404  opnneilv  49411  setrec1lem3  50191