Definition df-rex 3058

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 3049). (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 3057	. 2 wff ∃𝑥 ∈ 𝐴 𝜑
5	2	cv 1540	. . . . 5 class 𝑥
6	5, 3	wcel 2113	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wex 1780	. 2 wff ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 206	1 wff (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  ralnex  3059  rexex  3063  rextru  3064  reximi2  3066  rexbii2  3076  rexlimiva  3126  reximdv2  3143  rexbidv2  3153  r19.41v  3163  r3ex  3172  reeanlem  3204  risset  3208  cbvrexvw  3212  rspe  3223  r19.23t  3229  r19.41  3237  reximd2a  3243  rexbida  3245  nfre1  3258  rexcom4  3260  r19.12  3282  rexeq  3289  rexeqfOLD  3324  reu5  3349  rmo5  3365  rexv  3465  2gencl  3480  3gencl  3481  rspce  3562  ceqsrexv  3606  rexab2  3654  rexrab2  3655  morex  3674  reu2  3680  reu6  3681  reu3  3682  2reuswap  3701  2reuswap2  3702  2reu5lem3  3712  2reu5  3713  2rmoswap  3716  ssrexf  3997  ssrexv  4000  rexss  4006  rexdifi  4099  rexun  4145  reuun2  4274  reuss2  4275  reupick  4278  reupick3  4279  euelss  4281  reximdva0  4304  n0rex  4306  n0el  4313  inn0f  4320  r19.2z  4444  r19.2zb  4445  rexsns  4623  exsnrex  4632  dfuni2  4860  eluni2  4862  elunirab  4873  iuncom4  4950  iunxiun  5047  axrep6  5228  axrep6OLD  5229  axsepgfromrep  5234  intexrab  5287  opeliunxp  5686  opeliun2xp  5687  xpiundi  5690  xpiundir  5691  ssrelrn  5838  dmuni  5858  rnmpt  5901  elrnmpt1  5904  dfima2  6015  dfima3  6016  elima2  6019  dfco2a  6198  imaco  6203  elsnxp  6243  dfpo2  6248  fvelima2  6880  dffo4  7042  dffo5  7043  abrexco  7184  isomin  7277  imaeqsexvOLD  7303  imaeqexov  7590  zfrep6  7893  opabex3d  7903  opabex3rd  7904  opabex3  7905  abexssex  7908  abexex  7909  frxp  8062  dfrecs3  8298  rdglim2  8357  oarec  8483  oeeu  8524  mapsnd  8816  mapsnend  8965  pssnn  9085  enfii  9102  enp1i  9170  unblem2  9184  pwfir  9208  dffi2  9314  marypha2lem4  9329  marypha2  9330  zfregcl  9487  zfregclOLD  9488  axinf2  9537  zfinf2  9539  brttrcl2  9611  ttrclselem2  9623  rankuni  9763  scott0  9786  cp  9791  bnd2  9793  infpwfien  9960  aceq1  10015  dfac5lem2  10022  dfac5lem3  10023  dfac2b  10029  kmlem3  10051  kmlem6  10054  kmlem8  10056  kmlem14  10062  infmap2  10115  ackbij2  10140  cfub  10147  cfval2  10158  cflim3  10160  cfss  10163  cfslb  10164  isf32lem9  10259  zorn2lem6  10399  iundom2g  10438  winalim2  10594  grothprim  10732  genpass  10907  nqpr  10912  1idpr  10927  ltexprlem4  10937  ltexprlem5  10938  reclem2pr  10946  axrrecex  11061  dedekind  11283  sup2  12085  infm3  12088  nnunb  12384  2rexuz  12800  nnwos  12815  xrsupsslem  13208  xrinfmsslem  13209  hashgt23el  14333  ishashinf  14372  wwlktovfo  14867  maxprmfct  16622  vdwapun  16888  vdwmc  16892  vdwmc2  16893  ram0  16936  imasleval  17447  mreexexlem2d  17553  dfiso2  17681  isssc  17729  drsdirfi  18213  dirge  18511  pwmnd  18847  psgnunilem4  19411  odcau  19518  ablfac2  20005  lspprat  21092  lidlnz  21181  isbasis2g  22864  tgval2  22872  ntreq0  22993  neitr  23096  cmpfi  23324  is1stc2  23358  2ndcsb  23365  2ndcsep  23375  1stcelcls  23377  hausmapdom  23416  isfbas2  23751  fbssint  23754  isfil2  23772  elfg  23787  fgcl  23794  uffix2  23840  alexsubALTlem4  23966  lpbl  24419  metustexhalf  24472  metuel2  24481  restmetu  24486  bcthlem5  25256  lrrecfr  27887  upgrex  29072  uvtx01vtx  29377  uhgrvd00  29515  wlkswwlksf1o  29859  wwlksnextsurj  29880  frcond3  30251  frgr3vlem2  30256  3vfriswmgrlem  30259  frgrncvvdeqlem9  30289  ubthlem1  30852  axhcompl-zf  30980  isch3  31223  shne0i  31430  cnlnssadj  32062  reuxfrdf  32472  rexunirn  32473  rmoxfrd  32474  dmrab  32478  abrexdomjm  32489  abrexexd  32491  iunrnmptss  32547  ac6mapd  32608  1stpreimas  32691  fpwrelmapffslem  32719  qsxpid  33334  krull  33451  zarclsint  33906  ordtconnlem1  33958  ddemeas  34270  omssubaddlem  34333  omssubadd  34334  eulerpartlemgvv  34410  tgoldbachgt  34697  bnj168  34763  bnj956  34809  bnj1098  34816  bnj1143  34823  bnj1146  34824  bnj1185  34826  bnj1196  34827  bnj600  34952  bnj849  34958  bnj906  34963  bnj916  34966  bnj983  34984  bnj984  34985  bnj1083  35011  bnj1176  35038  bnj1186  35040  bnj1189  35042  bnj1228  35044  bnj1253  35050  bnj1398  35067  bnj1463  35088  bnj1312  35091  bnj1514  35096  exdifsn  35112  r1filimi  35135  axregszf  35148  onvf1odlem1  35168  onvf1odlem2  35169  wevgblacfn  35174  lfuhgr3  35185  cusgredgex  35187  loop1cycl  35202  erdszelem10  35265  ptpconn  35298  rexxfr3dALT  35704  coep  35817  coepr  35818  dffr5  35819  opelco3  35840  dfon2lem8  35853  brimg  36000  dfrecs2  36015  dfrdg4  36016  ellines  36217  cbvrexvw2  36292  neifg  36436  bj-rexvw  36945  bj-gabima  37005  bj-snglc  37034  bj-snglss  37035  bj-rest10  37153  bj-restn0  37155  bj-restpw  37157  bj-rest0  37158  bj-restb  37159  bj-restuni  37162  bj-dfmpoa  37183  bj-finsumval0  37350  rnmptsn  37400  f1omptsnlem  37401  mptsnunlem  37403  topdifinffinlem  37412  isbasisrelowllem1  37420  isbasisrelowllem2  37421  relowlpssretop  37429  fvineqsneq  37477  pibt2  37482  poimirlem30  37710  abrexdom  37790  prdstotbnd  37854  elrnres  38330  eldmqsres2  38346  exanres  38353  rncnvepres  38361  rnxrnres  38466  1cossres  38551  eldm1cossres  38582  eldmqs1cossres  38777  disjlem17  38917  disjdmqscossss  38921  prtlem17  38995  prter2  39000  islshpat  39136  lsat0cv  39152  lshpsmreu  39228  atex  39525  islpln5  39654  islvol5  39698  pmapglb  39889  pmapglb2N  39890  pmapglb2xN  39891  elpaddn0  39919  pmapjat1  39972  polval2N  40025  osumcllem11N  40085  pexmidlem8N  40096  cdlemftr3  40684  dibelval3  41266  dibglbN  41285  dicelval3  41299  dihglbcpreN  41419  dihglb2  41461  dihjatcclem4  41540  mapdrvallem2  41764  mapdpglem3  41794  hdmapglem7a  42046  sticksstones3  42261  imaopab  42349  sn-sup2  42609  fimgmcyc  42652  prjspeclsp  42730  uniel  43334  nnoeomeqom  43429  tfsconcatlem  43453  tfsconcatrn  43459  tfsconcat0i  43462  rp-isfinite5  43634  rp-isfinite6  43635  minregex  43651  elintima  43770  iunrelexpuztr  43836  cotrclrcl  43859  neik0pk1imk0  44164  ntrneineine0lem  44200  ntrneineine1lem  44201  ntrneiel2  44203  cpcolld  44375  expandrexn  44408  ismnuprim  44411  rr-grothprimbi  44412  rr-groth  44416  ismnushort  44418  rr-grothshortbi  44420  rexbidar  44562  onfrALTlem5  44659  onfrALTlem2  44663  onfrALTlem1  44665  onfrALTlem5VD  45001  onfrALTlem2VD  45005  onfrALTlem1VD  45006  chordthmALT  45049  rspesbcd  45054  modelaxreplem3  45097  ssclaxsep  45099  permaxrep  45123  nregmodel  45134  rspcegf  45144  cncmpmax  45153  rfcnnnub  45157  nssrex  45207  eluni2f  45224  eliin2f  45225  suprnmpt  45295  founiiun0  45311  disjinfi  45313  ssfiunibd  45434  infrpge  45474  fsumiunss  45699  islpcn  45761  lptre2pt  45762  stoweidlem14  46136  stoweidlem34  46156  stoweidlem35  46157  stoweidlem43  46165  stoweidlem44  46166  stoweidlem50  46172  stoweidlem54  46176  stoweidlem56  46178  stoweidlem59  46181  stoweidlem60  46182  fourier2  46349  qndenserrnbllem  46416  qndenserrn  46421  sge0rpcpnf  46543  hoidmvval0b  46712  hoiqssbllem3  46746  chnsubseqword  47000  imasetpreimafvbijlemfv1  47527  nfermltl8rev  47866  nfermltl2rev  47867  nfermltlrev  47868  isubgredg  47990  gpg5edgnedg  48254  nn0mnd  48303  opncldeqv  49026  opnneilv  49033  setrec1lem3  49814