Definition df-rex 3057

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 3048). (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 3056	. 2 wff ∃𝑥 ∈ 𝐴 𝜑
5	2	cv 1540	. . . . 5 class 𝑥
6	5, 3	wcel 2111	. . . 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  3058  rexex  3062  rextru  3063  reximi2  3065  rexbii2  3075  rexlimiva  3125  reximdv2  3142  rexbidv2  3152  r19.41v  3162  r3ex  3171  reeanlem  3203  risset  3207  cbvrexvw  3211  rspe  3222  r19.23t  3228  r19.41  3236  reximd2a  3242  rexbida  3244  nfre1  3257  rexcom4  3259  r19.12  3281  rexeq  3288  rexeqfOLD  3323  reu5  3348  rmo5  3364  rexv  3464  2gencl  3479  3gencl  3480  rspce  3566  ceqsrexv  3610  rexab2  3658  rexrab2  3659  morex  3678  reu2  3684  reu6  3685  reu3  3686  2reuswap  3705  2reuswap2  3706  2reu5lem3  3716  2reu5  3717  2rmoswap  3720  ssrexf  4001  ssrexv  4004  rexss  4010  rexdifi  4100  rexun  4146  reuun2  4275  reuss2  4276  reupick  4279  reupick3  4280  euelss  4282  reximdva0  4305  n0rex  4307  n0el  4314  inn0f  4321  r19.2z  4445  r19.2zb  4446  rexsns  4624  exsnrex  4633  dfuni2  4861  eluni2  4863  elunirab  4874  iuncom4  4950  iunxiun  5045  axrep6  5226  axrep6OLD  5227  axsepgfromrep  5232  intexrab  5285  opeliunxp  5683  opeliun2xp  5684  xpiundi  5687  xpiundir  5688  ssrelrn  5834  dmuni  5854  rnmpt  5897  elrnmpt1  5900  dfima2  6011  dfima3  6012  elima2  6015  dfco2a  6193  imaco  6198  elsnxp  6238  dfpo2  6243  fvelima2  6874  dffo4  7036  dffo5  7037  abrexco  7178  isomin  7271  imaeqsexvOLD  7297  imaeqexov  7584  zfrep6  7887  opabex3d  7897  opabex3rd  7898  opabex3  7899  abexssex  7902  abexex  7903  frxp  8056  dfrecs3  8292  rdglim2  8351  oarec  8477  oeeu  8518  mapsnd  8810  mapsnend  8958  pssnn  9078  enfii  9095  enp1i  9163  unblem2  9177  pwfir  9201  dffi2  9307  marypha2lem4  9322  marypha2  9323  zfregcl  9480  zfregclOLD  9481  axinf2  9530  zfinf2  9532  brttrcl2  9604  ttrclselem2  9616  rankuni  9753  scott0  9776  cp  9781  bnd2  9783  infpwfien  9950  aceq1  10005  dfac5lem2  10012  dfac5lem3  10013  dfac2b  10019  kmlem3  10041  kmlem6  10044  kmlem8  10046  kmlem14  10052  infmap2  10105  ackbij2  10130  cfub  10137  cfval2  10148  cflim3  10150  cfss  10153  cfslb  10154  isf32lem9  10249  zorn2lem6  10389  iundom2g  10428  winalim2  10584  grothprim  10722  genpass  10897  nqpr  10902  1idpr  10917  ltexprlem4  10927  ltexprlem5  10928  reclem2pr  10936  axrrecex  11051  dedekind  11273  sup2  12075  infm3  12078  nnunb  12374  2rexuz  12795  nnwos  12810  xrsupsslem  13203  xrinfmsslem  13204  hashgt23el  14328  ishashinf  14367  wwlktovfo  14862  maxprmfct  16617  vdwapun  16883  vdwmc  16887  vdwmc2  16888  ram0  16931  imasleval  17442  mreexexlem2d  17548  dfiso2  17676  isssc  17724  drsdirfi  18208  dirge  18506  pwmnd  18842  psgnunilem4  19407  odcau  19514  ablfac2  20001  lspprat  21088  lidlnz  21177  isbasis2g  22861  tgval2  22869  ntreq0  22990  neitr  23093  cmpfi  23321  is1stc2  23355  2ndcsb  23362  2ndcsep  23372  1stcelcls  23374  hausmapdom  23413  isfbas2  23748  fbssint  23751  isfil2  23769  elfg  23784  fgcl  23791  uffix2  23837  alexsubALTlem4  23963  lpbl  24416  metustexhalf  24469  metuel2  24478  restmetu  24483  bcthlem5  25253  lrrecfr  27884  upgrex  29068  uvtx01vtx  29373  uhgrvd00  29511  wlkswwlksf1o  29855  wwlksnextsurj  29876  frcond3  30244  frgr3vlem2  30249  3vfriswmgrlem  30252  frgrncvvdeqlem9  30282  ubthlem1  30845  axhcompl-zf  30973  isch3  31216  shne0i  31423  cnlnssadj  32055  reuxfrdf  32465  rexunirn  32466  rmoxfrd  32467  dmrab  32471  abrexdomjm  32482  abrexexd  32484  iunrnmptss  32540  ac6mapd  32601  1stpreimas  32682  fpwrelmapffslem  32710  qsxpid  33322  krull  33439  zarclsint  33880  ordtconnlem1  33932  ddemeas  34244  omssubaddlem  34307  omssubadd  34308  eulerpartlemgvv  34384  tgoldbachgt  34671  bnj168  34737  bnj956  34783  bnj1098  34790  bnj1143  34797  bnj1146  34798  bnj1185  34800  bnj1196  34801  bnj600  34926  bnj849  34932  bnj906  34937  bnj916  34940  bnj983  34958  bnj984  34959  bnj1083  34985  bnj1176  35012  bnj1186  35014  bnj1189  35016  bnj1228  35018  bnj1253  35024  bnj1398  35041  bnj1463  35062  bnj1312  35065  bnj1514  35070  exdifsn  35086  r1filimi  35106  axregszf  35115  onvf1odlem1  35135  onvf1odlem2  35136  wevgblacfn  35141  lfuhgr3  35152  cusgredgex  35154  loop1cycl  35169  erdszelem10  35232  ptpconn  35265  rexxfr3dALT  35671  coep  35784  coepr  35785  dffr5  35786  opelco3  35807  dfon2lem8  35823  brimg  35970  dfrecs2  35983  dfrdg4  35984  ellines  36185  cbvrexvw2  36260  neifg  36404  bj-rexvw  36913  bj-gabima  36973  bj-snglc  37002  bj-snglss  37003  bj-rest10  37121  bj-restn0  37123  bj-restpw  37125  bj-rest0  37126  bj-restb  37127  bj-restuni  37130  bj-dfmpoa  37151  bj-finsumval0  37318  rnmptsn  37368  f1omptsnlem  37369  mptsnunlem  37371  topdifinffinlem  37380  isbasisrelowllem1  37388  isbasisrelowllem2  37389  relowlpssretop  37397  fvineqsneq  37445  pibt2  37450  poimirlem30  37689  abrexdom  37769  prdstotbnd  37833  elrnres  38305  eldmqsres2  38321  exanres  38328  rncnvepres  38336  rnxrnres  38430  1cossres  38465  eldm1cossres  38496  eldmqs1cossres  38696  disjlem17  38836  disjdmqscossss  38840  prtlem17  38914  prter2  38919  islshpat  39055  lsat0cv  39071  lshpsmreu  39147  atex  39444  islpln5  39573  islvol5  39617  pmapglb  39808  pmapglb2N  39809  pmapglb2xN  39810  elpaddn0  39838  pmapjat1  39891  polval2N  39944  osumcllem11N  40004  pexmidlem8N  40015  cdlemftr3  40603  dibelval3  41185  dibglbN  41204  dicelval3  41218  dihglbcpreN  41338  dihglb2  41380  dihjatcclem4  41459  mapdordlem2  41675  mapdrvallem2  41683  mapdpglem3  41713  hdmapglem7a  41965  sticksstones3  42180  imaopab  42263  sn-sup2  42523  fimgmcyc  42566  prjspeclsp  42644  uniel  43249  nnoeomeqom  43344  tfsconcatlem  43368  tfsconcatrn  43374  tfsconcat0i  43377  rp-isfinite5  43549  rp-isfinite6  43550  minregex  43566  elintima  43685  iunrelexpuztr  43751  cotrclrcl  43774  neik0pk1imk0  44079  ntrneineine0lem  44115  ntrneineine1lem  44116  ntrneiel2  44118  cpcolld  44290  expandrexn  44323  ismnuprim  44326  rr-grothprimbi  44327  rr-groth  44331  ismnushort  44333  rr-grothshortbi  44335  rexbidar  44477  onfrALTlem5  44574  onfrALTlem2  44578  onfrALTlem1  44580  onfrALTlem5VD  44916  onfrALTlem2VD  44920  onfrALTlem1VD  44921  chordthmALT  44964  rspesbcd  44969  modelaxreplem3  45012  ssclaxsep  45014  permaxrep  45038  nregmodel  45049  rspcegf  45059  cncmpmax  45068  rfcnnnub  45072  nssrex  45122  eluni2f  45139  eliin2f  45140  suprnmpt  45210  founiiun0  45226  disjinfi  45228  ssfiunibd  45349  infrpge  45389  fsumiunss  45614  islpcn  45676  lptre2pt  45677  stoweidlem14  46051  stoweidlem34  46071  stoweidlem35  46072  stoweidlem43  46080  stoweidlem44  46081  stoweidlem50  46087  stoweidlem54  46091  stoweidlem56  46093  stoweidlem59  46096  stoweidlem60  46097  fourier2  46264  qndenserrnbllem  46331  qndenserrn  46336  sge0rpcpnf  46458  hoidmvval0b  46627  hoiqssbllem3  46661  imasetpreimafvbijlemfv1  47433  nfermltl8rev  47772  nfermltl2rev  47773  nfermltlrev  47774  isubgredg  47896  gpg5edgnedg  48160  nn0mnd  48209  opncldeqv  48932  opnneilv  48939  setrec1lem3  49720