Definition df-rex 3055

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 3046). (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 3054	. 2 wff ∃𝑥 ∈ 𝐴 𝜑
5	2	cv 1539	. . . . 5 class 𝑥
6	5, 3	wcel 2109	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wex 1779	. 2 wff ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 206	1 wff (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  ralnex  3056  rexex  3060  rextru  3061  reximi2  3063  rexbii2  3073  rexlimiva  3127  reximdv2  3144  rexbidv2  3154  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  rexcomOLD  3268  r19.12  3290  rexeq  3297  cbvrexdva2OLD  3325  rexeqfOLD  3333  reu5  3358  rmo5  3376  rexv  3478  2gencl  3493  3gencl  3494  rspce  3580  ceqsrexv  3624  rexab2  3673  rexrab2  3674  morex  3693  reu2  3699  reu6  3700  reu3  3701  2reuswap  3720  2reuswap2  3721  2reu5lem3  3731  2reu5  3732  2rmoswap  3735  ssrexf  4016  ssrexv  4019  rexss  4025  rexdifi  4116  rexun  4162  reuun2  4291  reuss2  4292  reupick  4295  reupick3  4296  euelss  4298  reximdva0  4321  n0rex  4323  n0el  4330  inn0f  4337  r19.2z  4461  r19.2zb  4462  rexsns  4638  exsnrex  4647  dfuni2  4876  eluni2  4878  elunirab  4889  iuncom4  4967  iunxiun  5064  axrep6  5246  axrep6OLD  5247  axsepgfromrep  5252  intexrab  5305  opeliunxp  5708  opeliun2xp  5709  xpiundi  5712  xpiundir  5713  ssrelrn  5861  dmuni  5881  rnmpt  5924  elrnmpt1  5927  dfima2  6036  dfima3  6037  elima2  6040  dfco2a  6222  imaco  6227  elsnxp  6267  dfpo2  6272  fvelima2  6916  dffo4  7078  dffo5  7079  abrexco  7221  isomin  7315  imaeqsexvOLD  7341  imaeqexov  7630  zfrep6  7936  opabex3d  7947  opabex3rd  7948  opabex3  7949  abexssex  7952  abexex  7953  frxp  8108  dfrecs3  8344  rdglim2  8403  oarec  8529  oeeu  8570  mapsnd  8862  mapsnend  9010  pssnn  9138  enfii  9156  enp1i  9231  unblem2  9247  pwfir  9273  dffi2  9381  marypha2lem4  9396  marypha2  9397  zfregcl  9554  axinf2  9600  zfinf2  9602  brttrcl2  9674  ttrclselem2  9686  rankuni  9823  scott0  9846  cp  9851  bnd2  9853  infpwfien  10022  aceq1  10077  dfac5lem2  10084  dfac5lem3  10085  dfac2b  10091  kmlem3  10113  kmlem6  10116  kmlem8  10118  kmlem14  10124  infmap2  10177  ackbij2  10202  cfub  10209  cfval2  10220  cflim3  10222  cfss  10225  cfslb  10226  isf32lem9  10321  zorn2lem6  10461  iundom2g  10500  winalim2  10656  grothprim  10794  genpass  10969  nqpr  10974  1idpr  10989  ltexprlem4  10999  ltexprlem5  11000  reclem2pr  11008  axrrecex  11123  dedekind  11344  sup2  12146  infm3  12149  nnunb  12445  2rexuz  12866  nnwos  12881  xrsupsslem  13274  xrinfmsslem  13275  hashgt23el  14396  ishashinf  14435  cshwsexaOLD  14797  wwlktovfo  14931  maxprmfct  16686  vdwapun  16952  vdwmc  16956  vdwmc2  16957  ram0  17000  imasleval  17511  mreexexlem2d  17613  dfiso2  17741  isssc  17789  drsdirfi  18273  dirge  18569  pwmnd  18871  psgnunilem4  19434  odcau  19541  ablfac2  20028  lspprat  21070  lidlnz  21159  isbasis2g  22842  tgval2  22850  ntreq0  22971  neitr  23074  cmpfi  23302  is1stc2  23336  2ndcsb  23343  2ndcsep  23353  1stcelcls  23355  hausmapdom  23394  isfbas2  23729  fbssint  23732  isfil2  23750  elfg  23765  fgcl  23772  uffix2  23818  alexsubALTlem4  23944  lpbl  24398  metustexhalf  24451  metuel2  24460  restmetu  24465  bcthlem5  25235  lrrecfr  27857  upgrex  29026  uvtx01vtx  29331  uhgrvd00  29469  wlkswwlksf1o  29816  wwlksnextsurj  29837  frcond3  30205  frgr3vlem2  30210  3vfriswmgrlem  30213  frgrncvvdeqlem9  30243  ubthlem1  30806  axhcompl-zf  30934  isch3  31177  shne0i  31384  cnlnssadj  32016  reuxfrdf  32427  rexunirn  32428  rmoxfrd  32429  dmrab  32433  abrexdomjm  32443  abrexexd  32445  iunrnmptss  32501  ac6mapd  32556  1stpreimas  32636  fpwrelmapffslem  32662  qsxpid  33340  krull  33457  zarclsint  33869  ordtconnlem1  33921  ddemeas  34233  omssubaddlem  34297  omssubadd  34298  eulerpartlemgvv  34374  tgoldbachgt  34661  bnj168  34727  bnj956  34773  bnj1098  34780  bnj1143  34787  bnj1146  34788  bnj1185  34790  bnj1196  34791  bnj600  34916  bnj849  34922  bnj906  34927  bnj916  34930  bnj983  34948  bnj984  34949  bnj1083  34975  bnj1176  35002  bnj1186  35004  bnj1189  35006  bnj1228  35008  bnj1253  35014  bnj1398  35031  bnj1463  35052  bnj1312  35055  bnj1514  35060  exdifsn  35076  onvf1odlem1  35097  onvf1odlem2  35098  wevgblacfn  35103  lfuhgr3  35114  cusgredgex  35116  loop1cycl  35131  erdszelem10  35194  ptpconn  35227  rexxfr3dALT  35633  coep  35746  coepr  35747  dffr5  35748  opelco3  35769  dfon2lem8  35785  brimg  35932  dfrecs2  35945  dfrdg4  35946  ellines  36147  cbvrexvw2  36222  neifg  36366  bj-rexvw  36875  bj-gabima  36935  bj-snglc  36964  bj-snglss  36965  bj-rest10  37083  bj-restn0  37085  bj-restpw  37087  bj-rest0  37088  bj-restb  37089  bj-restuni  37092  bj-dfmpoa  37113  bj-finsumval0  37280  rnmptsn  37330  f1omptsnlem  37331  mptsnunlem  37333  topdifinffinlem  37342  isbasisrelowllem1  37350  isbasisrelowllem2  37351  relowlpssretop  37359  fvineqsneq  37407  pibt2  37412  poimirlem30  37651  abrexdom  37731  prdstotbnd  37795  elrnres  38267  eldmqsres2  38283  exanres  38290  rncnvepres  38298  rnxrnres  38392  1cossres  38427  eldm1cossres  38458  eldmqs1cossres  38658  disjlem17  38798  disjdmqscossss  38802  prtlem17  38876  prter2  38881  islshpat  39017  lsat0cv  39033  lshpsmreu  39109  atex  39407  islpln5  39536  islvol5  39580  pmapglb  39771  pmapglb2N  39772  pmapglb2xN  39773  elpaddn0  39801  pmapjat1  39854  polval2N  39907  osumcllem11N  39967  pexmidlem8N  39978  cdlemftr3  40566  dibelval3  41148  dibglbN  41167  dicelval3  41181  dihglbcpreN  41301  dihglb2  41343  dihjatcclem4  41422  mapdordlem2  41638  mapdrvallem2  41646  mapdpglem3  41676  hdmapglem7a  41928  sticksstones3  42143  imaopab  42226  sn-sup2  42486  fimgmcyc  42529  prjspeclsp  42607  uniel  43213  nnoeomeqom  43308  tfsconcatlem  43332  tfsconcatrn  43338  tfsconcat0i  43341  rp-isfinite5  43513  rp-isfinite6  43514  minregex  43530  elintima  43649  iunrelexpuztr  43715  cotrclrcl  43738  neik0pk1imk0  44043  ntrneineine0lem  44079  ntrneineine1lem  44080  ntrneiel2  44082  cpcolld  44254  expandrexn  44287  ismnuprim  44290  rr-grothprimbi  44291  rr-groth  44295  ismnushort  44297  rr-grothshortbi  44299  rexbidar  44442  onfrALTlem5  44539  onfrALTlem2  44543  onfrALTlem1  44545  onfrALTlem5VD  44881  onfrALTlem2VD  44885  onfrALTlem1VD  44886  chordthmALT  44929  rspesbcd  44934  modelaxreplem3  44977  ssclaxsep  44979  permaxrep  45003  nregmodel  45014  rspcegf  45024  cncmpmax  45033  rfcnnnub  45037  nssrex  45087  eluni2f  45104  eliin2f  45105  suprnmpt  45175  founiiun0  45191  disjinfi  45193  ssfiunibd  45314  infrpge  45354  fsumiunss  45580  islpcn  45644  lptre2pt  45645  stoweidlem14  46019  stoweidlem34  46039  stoweidlem35  46040  stoweidlem43  46048  stoweidlem44  46049  stoweidlem50  46055  stoweidlem54  46059  stoweidlem56  46061  stoweidlem59  46064  stoweidlem60  46065  fourier2  46232  qndenserrnbllem  46299  qndenserrn  46304  sge0rpcpnf  46426  hoidmvval0b  46595  hoiqssbllem3  46629  imasetpreimafvbijlemfv1  47408  nfermltl8rev  47747  nfermltl2rev  47748  nfermltlrev  47749  isubgredg  47870  nn0mnd  48171  opncldeqv  48894  opnneilv  48901  setrec1lem3  49682