Definition df-rex 3087

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 3077). (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 3086	. 2 wff ∃𝑥 ∈ 𝐴 𝜑
5	2	cv 1569	. . . . 5 class 𝑥
6	5, 3	wcel 2145	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 401	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wex 1812	. 2 wff ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 209	1 wff (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is used by:  ralnex  3088  rexex  3092  rextru  3093  reximi2  3095  rexbii2  3105  rexlimiva  3155  reximdv2  3172  rexbidv2  3182  r19.41v  3192  r3ex  3201  reeanlem  3233  risset  3237  cbvrexvw  3241  rspe  3252  r19.23t  3258  r19.41  3266  reximd2a  3272  rexbida  3274  nfre1  3287  rexcom4  3289  r19.12  3311  rexeq  3315  reu5  3367  rmo5  3383  rexv  3477  2gencl  3492  3gencl  3493  rspce  3565  ceqsrexv  3608  rexab2  3656  rexrab2  3657  morex  3676  reu2  3682  reu6  3683  reu3  3684  2reuswap  3703  2reuswap2  3704  2reu5lem3  3714  2reu5  3715  2rmoswap  3718  nssrex  3995  ssrexf  3997  ssrexv  4000  rexss  4004  rexdifi  4096  rexun  4141  reuun2  4270  reuss2  4271  reupick  4274  reupick3  4275  euelss  4277  reximdva0  4302  n0rex  4304  n0el  4311  inn0f  4318  r19.2z  4454  rexsns  4631  exsnrex  4640  dfuni2  4868  eluni2  4870  elunirab  4881  iuncom4  4959  iunxiun  5056  axrep6  5239  replem  5240  axsepgfromrep  5246  intexrab  5307  opeliunxp  5714  opeliun2xp  5715  xpiundi  5718  xpiundir  5719  ssrelrn  5872  dmuni  5892  rnmpt  5935  elrnmpt1  5938  dfima2  6052  dfima3  6053  elima2  6056  dfco2a  6236  imaco  6241  elsnxp  6283  dfpo2  6288  fvelima2  6925  dffo4  7091  dffo5  7092  abrexco  7236  isomin  7333  imaeqexov  7647  zfrep6OLD  7950  opabex3d  7960  opabex3rd  7961  opabex3  7962  abexssex  7965  abexex  7966  frxp  8121  dfrecs3  8358  rdglim2  8418  oarec  8548  oeeu  8590  mapsnd  8892  mapsnend  9042  pssnn  9162  enfii  9179  enp1i  9248  unblem2  9263  pwfir  9286  dffi2  9393  marypha2lem4  9408  marypha2  9409  zfregcl  9566  zfregclOLD  9567  axinf2  9619  zfinf2  9621  brttrcl2  9693  ttrclselem2  9705  rankuni  9852  r1filimi  9876  scott0b  9908  scott0OLD  9909  cp  9925  bnd2  9927  setrec1lem3  9940  infpwfien  10112  aceq1  10167  dfac5lem2  10174  dfac5lem3  10175  dfac2b  10180  kmlem3  10202  kmlem6  10205  kmlem8  10207  kmlem14  10213  infmap2  10266  ackbij2  10291  cfub  10297  cfval2  10309  cflim3  10311  cfss  10314  cfslb  10315  isf32lem9  10410  zorn2lem6  10550  iundom2g  10595  winalim2  10752  grothprim  10890  genpass  11065  nqpr  11070  1idpr  11085  ltexprlem4  11095  ltexprlem5  11096  reclem2pr  11104  axrrecex  11219  dedekind  11444  sup2  12242  infm3  12245  nnunb  12571  2rexuz  12996  nnwos  13011  xrsupsslem  13406  xrinfmsslem  13407  hashgt23el  14536  ishashinf  14575  wwlktovfo  15078  maxprmfct  16847  vdwapun  17113  vdwmc  17117  vdwmc2  17118  ram0  17161  imasleval  17674  mreexexlem2d  17780  dfiso2  17908  isssc  17956  drsdirfi  18440  dirge  18738  pwmnd  19104  qsxpid  19348  psgnunilem4  19672  odcau  19779  ablfac2  20266  lspprat  21392  lidlnz  21491  isbasis2g  23227  tgval2  23235  ntreq0  23356  neitr  23459  cmpfi  23687  is1stc2  23721  2ndcsb  23728  2ndcsep  23739  1stcelcls  23741  hausmapdom  23780  isfbas2  24115  fbssint  24118  isfil2  24136  elfg  24151  fgcl  24158  uffix2  24204  alexsubALTlem4  24330  lpbl  24783  metustexhalf  24836  metuel2  24845  restmetu  24850  bcthlem5  25610  lrrecfr  28262  upgrex  29603  lfuhgr3  29661  uvtx01vtx  29911  uhgrvd00  30048  wlkswwlksf1o  30401  wwlksnextsurj  30422  loop1cycl  30677  frcond3  30803  frgr3vlem2  30808  3vfriswmgrlem  30811  frgrncvvdeqlem9  30841  ubthlem1  31405  axhcompl-zf  31533  isch3  31776  shne0i  31983  cnlnssadj  32615  reuxfrdf  33020  rexunirn  33021  rmoxfrd  33022  dmrab  33026  abrexdomjm  33036  abrexexd  33038  iunrnmptss  33092  ac6mapd  33150  1stpreimas  33232  fpwrelmapffslem  33257  krull  33936  zarclsint  34437  ordtconnlem1  34489  ddemeas  34802  omssubaddlem  34865  omssubadd  34866  eulerpartlemgvv  34942  tgoldbachgt  35226  bnj168  35295  bnj956  35341  bnj1098  35348  bnj1143  35354  bnj1146  35355  bnj1185  35357  bnj1196  35358  bnj600  35483  bnj849  35489  bnj906  35494  bnj916  35497  bnj983  35515  bnj984  35516  bnj1083  35542  bnj1176  35569  bnj1186  35571  bnj1189  35573  bnj1228  35575  bnj1253  35581  bnj1398  35598  bnj1463  35619  bnj1312  35622  bnj1514  35627  exdifsn  35644  axprALT2  35664  axregszf  35722  karddom  35754  kardsdom  35755  kardfi  35763  onvf1odlem1  35807  onvf1odlem2  35808  wevgblacfn  35815  cusgredgex  35827  erdszelem10  35886  ptpconn  35919  rexxfr3dALT  36325  coep  36438  coepr  36439  dffr5  36440  opelco3  36461  dfon2lem8  36474  brimg  36621  dfrecs2  36636  dfrdg4  36637  ellines  36839  cbvrexvw2  36938  neifg  37081  regsfromunir1  37250  bj-rexvw  37714  bj-gabima  37775  bj-snglc  37804  bj-snglss  37805  bj-axseprep  37910  bj-axreprepsep  37911  bj-rest10  37929  bj-restn0  37931  bj-restpw  37933  bj-rest0  37934  bj-restb  37935  bj-restuni  37938  bj-dfmpoa  37959  bj-finsumval0  38126  rnmptsn  38178  f1omptsnlem  38179  mptsnunlem  38181  topdifinffinlem  38190  isbasisrelowllem1  38198  isbasisrelowllem2  38199  relowlpssretop  38207  fvineqsneq  38255  pibt2  38260  poimirlem30  38488  negprop  38563  impprop  38564  dfprop1  38565  abrexdom  38584  prdstotbnd  38648  elrnres  39130  eldmqsres2  39146  exanres  39153  rncnvepres  39161  rnxrnres  39274  1cossres  39371  eldm1cossres  39402  eldmqs1cossres  39596  disjlem17  39754  disjdmqscossss  39758  prtlem17  39853  prter2  39858  islshpat  39994  lsat0cv  40010  lshpsmreu  40086  atex  40383  islpln5  40512  islvol5  40556  pmapglb  40747  pmapglb2N  40748  pmapglb2xN  40749  elpaddn0  40777  pmapjat1  40830  polval2N  40883  osumcllem11N  40943  pexmidlem8N  40954  cdlemftr3  41542  dibelval3  42124  dibglbN  42143  dicelval3  42157  dihglbcpreN  42277  dihglb2  42319  dihjatcclem4  42398  mapdrvallem2  42622  mapdpglem3  42652  hdmapglem7a  42904  sticksstones3  43118  imaopab  43205  sn-sup2  43483  fimgmcyc  43520  prjspeclsp  43562  uniel  44162  nnoeomeqom  44257  tfsconcatlem  44281  tfsconcatrn  44287  tfsconcat0i  44290  rp-isfinite5  44461  rp-isfinite6  44462  minregex  44478  elintima  44597  iunrelexpuztr  44663  cotrclrcl  44686  neik0pk1imk0  44991  ntrneineine0lem  45027  ntrneineine1lem  45028  ntrneiel2  45030  cpcolld  45186  expandrexn  45219  ismnuprim  45222  rr-grothprimbi  45223  rr-groth  45227  ismnushort  45229  rr-grothshortbi  45231  rexbidar  45373  onfrALTlem5  45469  onfrALTlem2  45473  onfrALTlem1  45475  onfrALTlem5VD  45811  onfrALTlem2VD  45815  onfrALTlem1VD  45816  chordthmALT  45859  rspesbcd  45864  modelaxreplem3  45907  ssclaxsep  45909  permaxrep  45933  nregmodel  45944  rspcegf  45961  cncmpmax  45970  rfcnnnub  45974  eluni2f  46039  eliin2f  46040  suprnmpt  46110  founiiun0  46126  disjinfi  46128  ssfiunibd  46246  infrpge  46285  fsumiunss  46509  islpcn  46571  lptre2pt  46572  stoweidlem14  46946  stoweidlem34  46966  stoweidlem35  46967  stoweidlem43  46975  stoweidlem44  46976  stoweidlem50  46982  stoweidlem54  46986  stoweidlem56  46988  stoweidlem59  46991  stoweidlem60  46992  fourier2  47159  qndenserrnbllem  47226  qndenserrn  47231  sge0rpcpnf  47353  hoidmvval0b  47522  hoiqssbllem3  47556  tmachlem-exagreecover  47878  imasetpreimafvbijlemfv1  48407  nfermltl8rev  48762  nfermltl2rev  48763  nfermltlrev  48764  isubgredg  48886  gpg5edgnedg  49150  nn0mnd  49198  opncldbid  49932  opnneilv  49939  dfrals2  50808