Definition df-rex 3088

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 3078). (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 3087	. 2 wff ∃𝑥 ∈ 𝐴 𝜑
5	2	cv 1567	. . . . 5 class 𝑥
6	5, 3	wcel 2141	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 400	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wex 1807	. 2 wff ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 209	1 wff (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  ralnex  3089  rexex  3093  rextru  3094  reximi2  3096  rexbii2  3106  rexlimiva  3156  reximdv2  3173  rexbidv2  3183  r19.41v  3193  r3ex  3202  reeanlem  3234  risset  3238  cbvrexvw  3242  rspe  3253  r19.23t  3259  r19.41  3267  reximd2a  3273  rexbida  3275  nfre1  3288  rexcom4  3290  r19.12  3312  rexeq  3317  reu5  3369  rmo5  3385  rexv  3480  2gencl  3495  3gencl  3496  rspce  3569  ceqsrexv  3613  rexab2  3661  rexrab2  3662  morex  3681  reu2  3687  reu6  3688  reu3  3689  2reuswap  3708  2reuswap2  3709  2reu5lem3  3719  2reu5  3720  2rmoswap  3723  nssrex  4001  ssrexf  4003  ssrexv  4006  rexss  4010  rexdifi  4103  rexun  4148  reuun2  4277  reuss2  4278  reupick  4281  reupick3  4282  euelss  4284  reximdva0  4309  n0rex  4311  n0el  4318  inn0f  4325  r19.2z  4459  rexsns  4636  exsnrex  4645  dfuni2  4873  eluni2  4875  elunirab  4886  iuncom4  4964  iunxiun  5062  axrep6  5246  axrep6OLD  5247  replem  5248  axsepgfromrep  5254  intexrab  5317  opeliunxp  5728  opeliun2xp  5729  xpiundi  5732  xpiundir  5733  ssrelrn  5884  dmuni  5904  rnmpt  5947  elrnmpt1  5950  dfima2  6064  dfima3  6065  elima2  6068  dfco2a  6247  imaco  6252  elsnxp  6292  dfpo2  6297  fvelima2  6933  dffo4  7098  dffo5  7099  abrexco  7242  isomin  7335  imaeqsexvOLD  7361  imaeqexov  7648  zfrep6OLD  7951  opabex3d  7961  opabex3rd  7962  opabex3  7963  abexssex  7966  abexex  7967  frxp  8121  dfrecs3  8358  rdglim2  8418  oarec  8546  oeeu  8588  mapsnd  8883  mapsnend  9032  pssnn  9152  enfii  9169  enp1i  9238  unblem2  9252  pwfir  9275  dffi2  9382  marypha2lem4  9397  marypha2  9398  zfregcl  9555  zfregclOLD  9556  axinf2  9608  zfinf2  9610  brttrcl2  9682  ttrclselem2  9694  rankuni  9834  scott0  9859  cp  9876  bnd2  9878  infpwfien  10045  aceq1  10100  dfac5lem2  10107  dfac5lem3  10108  dfac2b  10113  kmlem3  10135  kmlem6  10138  kmlem8  10140  kmlem14  10146  infmap2  10199  ackbij2  10224  cfub  10231  cfval2  10243  cflim3  10245  cfss  10248  cfslb  10249  isf32lem9  10344  zorn2lem6  10484  iundom2g  10523  winalim2  10680  grothprim  10818  genpass  10993  nqpr  10998  1idpr  11013  ltexprlem4  11023  ltexprlem5  11024  reclem2pr  11032  axrrecex  11147  dedekind  11372  sup2  12170  infm3  12173  nnunb  12499  2rexuz  12923  nnwos  12938  xrsupsslem  13332  xrinfmsslem  13333  hashgt23el  14460  ishashinf  14499  wwlktovfo  14994  maxprmfct  16767  vdwapun  17033  vdwmc  17037  vdwmc2  17038  ram0  17081  imasleval  17594  mreexexlem2d  17700  dfiso2  17828  isssc  17876  drsdirfi  18360  dirge  18658  pwmnd  18998  qsxpid  19242  psgnunilem4  19566  odcau  19673  ablfac2  20160  lspprat  21256  lidlnz  21355  isbasis2g  23084  tgval2  23092  ntreq0  23213  neitr  23316  cmpfi  23544  is1stc2  23578  2ndcsb  23585  2ndcsep  23595  1stcelcls  23597  hausmapdom  23636  isfbas2  23971  fbssint  23974  isfil2  23992  elfg  24007  fgcl  24014  uffix2  24060  alexsubALTlem4  24186  lpbl  24639  metustexhalf  24692  metuel2  24701  restmetu  24706  bcthlem5  25466  lrrecfr  28112  upgrex  29408  uvtx01vtx  29713  uhgrvd00  29850  wlkswwlksf1o  30194  wwlksnextsurj  30215  frcond3  30586  frgr3vlem2  30591  3vfriswmgrlem  30594  frgrncvvdeqlem9  30624  ubthlem1  31188  axhcompl-zf  31316  isch3  31559  shne0i  31766  cnlnssadj  32398  reuxfrdf  32803  rexunirn  32804  rmoxfrd  32805  dmrab  32809  abrexdomjm  32819  abrexexd  32821  iunrnmptss  32876  ac6mapd  32934  1stpreimas  33017  fpwrelmapffslem  33043  krull  33727  zarclsint  34228  ordtconnlem1  34280  ddemeas  34592  omssubaddlem  34655  omssubadd  34656  eulerpartlemgvv  34732  tgoldbachgt  35016  bnj168  35085  bnj956  35131  bnj1098  35138  bnj1143  35144  bnj1146  35145  bnj1185  35147  bnj1196  35148  bnj600  35273  bnj849  35279  bnj906  35284  bnj916  35287  bnj983  35305  bnj984  35306  bnj1083  35332  bnj1176  35359  bnj1186  35361  bnj1189  35363  bnj1228  35365  bnj1253  35371  bnj1398  35388  bnj1463  35409  bnj1312  35412  bnj1514  35417  exdifsn  35433  r1filimi  35461  axprALT2  35467  axregszf  35496  karddom  35528  kardsdom  35529  kardfi  35537  onvf1odlem1  35541  onvf1odlem2  35542  wevgblacfn  35549  lfuhgr3  35566  cusgredgex  35568  loop1cycl  35583  erdszelem10  35646  ptpconn  35679  rexxfr3dALT  36085  coep  36198  coepr  36199  dffr5  36200  opelco3  36221  dfon2lem8  36234  brimg  36381  dfrecs2  36396  dfrdg4  36397  ellines  36598  cbvrexvw2  36683  neifg  36826  regsfromunir1  36995  bj-rexvw  37459  bj-gabima  37520  bj-snglc  37549  bj-snglss  37550  bj-axseprep  37655  bj-axreprepsep  37656  bj-rest10  37674  bj-restn0  37676  bj-restpw  37678  bj-rest0  37679  bj-restb  37680  bj-restuni  37683  bj-dfmpoa  37704  bj-finsumval0  37873  rnmptsn  37925  f1omptsnlem  37926  mptsnunlem  37928  topdifinffinlem  37937  isbasisrelowllem1  37945  isbasisrelowllem2  37946  relowlpssretop  37954  fvineqsneq  38002  pibt2  38007  poimirlem30  38245  abrexdom  38325  prdstotbnd  38389  elrnres  38873  eldmqsres2  38889  exanres  38896  rncnvepres  38904  rnxrnres  39017  1cossres  39114  eldm1cossres  39145  eldmqs1cossres  39339  disjlem17  39497  disjdmqscossss  39501  prtlem17  39596  prter2  39601  islshpat  39737  lsat0cv  39753  lshpsmreu  39829  atex  40126  islpln5  40255  islvol5  40299  pmapglb  40490  pmapglb2N  40491  pmapglb2xN  40492  elpaddn0  40520  pmapjat1  40573  polval2N  40626  osumcllem11N  40686  pexmidlem8N  40697  cdlemftr3  41285  dibelval3  41867  dibglbN  41886  dicelval3  41900  dihglbcpreN  42020  dihglb2  42062  dihjatcclem4  42141  mapdrvallem2  42365  mapdpglem3  42395  hdmapglem7a  42647  sticksstones3  42861  imaopab  42948  sn-sup2  43211  fimgmcyc  43250  prjspeclsp  43292  uniel  43892  nnoeomeqom  43987  tfsconcatlem  44011  tfsconcatrn  44017  tfsconcat0i  44020  rp-isfinite5  44191  rp-isfinite6  44192  minregex  44208  elintima  44327  iunrelexpuztr  44393  cotrclrcl  44416  neik0pk1imk0  44721  ntrneineine0lem  44757  ntrneineine1lem  44758  ntrneiel2  44760  cpcolld  44916  expandrexn  44949  ismnuprim  44952  rr-grothprimbi  44953  rr-groth  44957  ismnushort  44959  rr-grothshortbi  44961  rexbidar  45103  onfrALTlem5  45199  onfrALTlem2  45203  onfrALTlem1  45205  onfrALTlem5VD  45541  onfrALTlem2VD  45545  onfrALTlem1VD  45546  chordthmALT  45589  rspesbcd  45594  modelaxreplem3  45637  ssclaxsep  45639  permaxrep  45663  nregmodel  45674  rspcegf  45691  cncmpmax  45700  rfcnnnub  45704  eluni2f  45769  eliin2f  45770  suprnmpt  45840  founiiun0  45856  disjinfi  45858  ssfiunibd  45976  infrpge  46015  fsumiunss  46239  islpcn  46301  lptre2pt  46302  stoweidlem14  46676  stoweidlem34  46696  stoweidlem35  46697  stoweidlem43  46705  stoweidlem44  46706  stoweidlem50  46712  stoweidlem54  46716  stoweidlem56  46718  stoweidlem59  46721  stoweidlem60  46722  fourier2  46889  qndenserrnbllem  46956  qndenserrn  46961  sge0rpcpnf  47083  hoidmvval0b  47252  hoiqssbllem3  47286  chnsubseqword  47542  imasetpreimafvbijlemfv1  48097  nfermltl8rev  48452  nfermltl2rev  48453  nfermltlrev  48454  isubgredg  48576  gpg5edgnedg  48840  nn0mnd  48889  opncldeqv  49625  opnneilv  49632  setrec1lem3  50412  dfrals2  50513