Definition df-rex 3089

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 3079). (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 3088	. 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  3090  rexex  3094  rextru  3095  reximi2  3097  rexbii2  3107  rexlimiva  3157  reximdv2  3174  rexbidv2  3184  r19.41v  3194  r3ex  3203  reeanlem  3235  risset  3239  cbvrexvw  3243  rspe  3254  r19.23t  3260  r19.41  3268  reximd2a  3274  rexbida  3276  nfre1  3289  rexcom4  3291  r19.12  3313  rexeq  3317  reu5  3369  rmo5  3385  rexv  3480  2gencl  3495  3gencl  3496  rspce  3568  ceqsrexv  3612  rexab2  3660  rexrab2  3661  morex  3680  reu2  3686  reu6  3687  reu3  3688  2reuswap  3707  2reuswap2  3708  2reu5lem3  3718  2reu5  3719  2rmoswap  3722  nssrex  3999  ssrexf  4001  ssrexv  4004  rexss  4008  rexdifi  4100  rexun  4145  reuun2  4274  reuss2  4275  reupick  4278  reupick3  4279  euelss  4281  reximdva0  4306  n0rex  4308  n0el  4315  inn0f  4322  r19.2z  4458  rexsns  4635  exsnrex  4644  dfuni2  4872  eluni2  4874  elunirab  4885  iuncom4  4963  iunxiun  5061  axrep6  5245  axrep6OLD  5246  replem  5247  axsepgfromrep  5253  intexrab  5315  opeliunxp  5726  opeliun2xp  5727  xpiundi  5730  xpiundir  5731  ssrelrn  5882  dmuni  5902  rnmpt  5945  elrnmpt1  5948  dfima2  6062  dfima3  6063  elima2  6066  dfco2a  6246  imaco  6251  elsnxp  6293  dfpo2  6298  fvelima2  6934  dffo4  7099  dffo5  7100  abrexco  7244  isomin  7341  imaeqexov  7655  zfrep6OLD  7955  opabex3d  7965  opabex3rd  7966  opabex3  7967  abexssex  7970  abexex  7971  frxp  8127  dfrecs3  8364  rdglim2  8424  oarec  8552  oeeu  8594  mapsnd  8896  mapsnend  9046  pssnn  9166  enfii  9183  enp1i  9252  unblem2  9266  pwfir  9289  dffi2  9396  marypha2lem4  9411  marypha2  9412  zfregcl  9569  zfregclOLD  9570  axinf2  9622  zfinf2  9624  brttrcl2  9696  ttrclselem2  9708  rankuni  9848  scott0b  9879  scott0OLD  9880  cp  9896  bnd2  9898  infpwfien  10068  aceq1  10123  dfac5lem2  10130  dfac5lem3  10131  dfac2b  10136  kmlem3  10158  kmlem6  10161  kmlem8  10163  kmlem14  10169  infmap2  10222  ackbij2  10247  cfub  10253  cfval2  10265  cflim3  10267  cfss  10270  cfslb  10271  isf32lem9  10366  zorn2lem6  10506  iundom2g  10551  winalim2  10708  grothprim  10846  genpass  11021  nqpr  11026  1idpr  11041  ltexprlem4  11051  ltexprlem5  11052  reclem2pr  11060  axrrecex  11175  dedekind  11400  sup2  12198  infm3  12201  nnunb  12527  2rexuz  12952  nnwos  12967  xrsupsslem  13361  xrinfmsslem  13362  hashgt23el  14491  ishashinf  14530  wwlktovfo  15033  maxprmfct  16804  vdwapun  17070  vdwmc  17074  vdwmc2  17075  ram0  17118  imasleval  17631  mreexexlem2d  17737  dfiso2  17865  isssc  17913  drsdirfi  18397  dirge  18695  pwmnd  19057  qsxpid  19301  psgnunilem4  19625  odcau  19732  ablfac2  20219  lspprat  21341  lidlnz  21440  isbasis2g  23174  tgval2  23182  ntreq0  23303  neitr  23406  cmpfi  23634  is1stc2  23668  2ndcsb  23675  2ndcsep  23686  1stcelcls  23688  hausmapdom  23727  isfbas2  24062  fbssint  24065  isfil2  24083  elfg  24098  fgcl  24105  uffix2  24151  alexsubALTlem4  24277  lpbl  24730  metustexhalf  24783  metuel2  24792  restmetu  24797  bcthlem5  25557  lrrecfr  28206  upgrex  29535  lfuhgr3  29593  uvtx01vtx  29843  uhgrvd00  29980  wlkswwlksf1o  30333  wwlksnextsurj  30354  loop1cycl  30609  frcond3  30735  frgr3vlem2  30740  3vfriswmgrlem  30743  frgrncvvdeqlem9  30773  ubthlem1  31337  axhcompl-zf  31465  isch3  31708  shne0i  31915  cnlnssadj  32547  reuxfrdf  32952  rexunirn  32953  rmoxfrd  32954  dmrab  32958  abrexdomjm  32968  abrexexd  32970  iunrnmptss  33025  ac6mapd  33083  1stpreimas  33165  fpwrelmapffslem  33190  krull  33868  zarclsint  34369  ordtconnlem1  34421  ddemeas  34734  omssubaddlem  34797  omssubadd  34798  eulerpartlemgvv  34874  tgoldbachgt  35158  bnj168  35227  bnj956  35273  bnj1098  35280  bnj1143  35286  bnj1146  35287  bnj1185  35289  bnj1196  35290  bnj600  35415  bnj849  35421  bnj906  35426  bnj916  35429  bnj983  35447  bnj984  35448  bnj1083  35474  bnj1176  35501  bnj1186  35503  bnj1189  35505  bnj1228  35507  bnj1253  35513  bnj1398  35530  bnj1463  35551  bnj1312  35554  bnj1514  35559  exdifsn  35576  r1filimi  35598  axprALT2  35604  axregszf  35642  karddom  35674  kardsdom  35675  kardfi  35683  onvf1odlem1  35687  onvf1odlem2  35688  wevgblacfn  35695  cusgredgex  35707  erdszelem10  35766  ptpconn  35799  rexxfr3dALT  36205  coep  36318  coepr  36319  dffr5  36320  opelco3  36341  dfon2lem8  36354  brimg  36501  dfrecs2  36516  dfrdg4  36517  ellines  36719  cbvrexvw2  36834  neifg  36977  regsfromunir1  37146  bj-rexvw  37610  bj-gabima  37671  bj-snglc  37700  bj-snglss  37701  bj-axseprep  37806  bj-axreprepsep  37807  bj-rest10  37825  bj-restn0  37827  bj-restpw  37829  bj-rest0  37830  bj-restb  37831  bj-restuni  37834  bj-dfmpoa  37855  bj-finsumval0  38024  rnmptsn  38076  f1omptsnlem  38077  mptsnunlem  38079  topdifinffinlem  38088  isbasisrelowllem1  38096  isbasisrelowllem2  38097  relowlpssretop  38105  fvineqsneq  38153  pibt2  38158  poimirlem30  38386  abrexdom  38467  prdstotbnd  38531  elrnres  39013  eldmqsres2  39029  exanres  39036  rncnvepres  39044  rnxrnres  39157  1cossres  39254  eldm1cossres  39285  eldmqs1cossres  39479  disjlem17  39637  disjdmqscossss  39641  prtlem17  39736  prter2  39741  islshpat  39877  lsat0cv  39893  lshpsmreu  39969  atex  40266  islpln5  40395  islvol5  40439  pmapglb  40630  pmapglb2N  40631  pmapglb2xN  40632  elpaddn0  40660  pmapjat1  40713  polval2N  40766  osumcllem11N  40826  pexmidlem8N  40837  cdlemftr3  41425  dibelval3  42007  dibglbN  42026  dicelval3  42040  dihglbcpreN  42160  dihglb2  42202  dihjatcclem4  42281  mapdrvallem2  42505  mapdpglem3  42535  hdmapglem7a  42787  sticksstones3  43001  imaopab  43088  sn-sup2  43366  fimgmcyc  43403  prjspeclsp  43445  uniel  44045  nnoeomeqom  44140  tfsconcatlem  44164  tfsconcatrn  44170  tfsconcat0i  44173  rp-isfinite5  44344  rp-isfinite6  44345  minregex  44361  elintima  44480  iunrelexpuztr  44546  cotrclrcl  44569  neik0pk1imk0  44874  ntrneineine0lem  44910  ntrneineine1lem  44911  ntrneiel2  44913  cpcolld  45069  expandrexn  45102  ismnuprim  45105  rr-grothprimbi  45106  rr-groth  45110  ismnushort  45112  rr-grothshortbi  45114  rexbidar  45256  onfrALTlem5  45352  onfrALTlem2  45356  onfrALTlem1  45358  onfrALTlem5VD  45694  onfrALTlem2VD  45698  onfrALTlem1VD  45699  chordthmALT  45742  rspesbcd  45747  modelaxreplem3  45790  ssclaxsep  45792  permaxrep  45816  nregmodel  45827  rspcegf  45844  cncmpmax  45853  rfcnnnub  45857  eluni2f  45922  eliin2f  45923  suprnmpt  45993  founiiun0  46009  disjinfi  46011  ssfiunibd  46129  infrpge  46168  fsumiunss  46392  islpcn  46454  lptre2pt  46455  stoweidlem14  46829  stoweidlem34  46849  stoweidlem35  46850  stoweidlem43  46858  stoweidlem44  46859  stoweidlem50  46865  stoweidlem54  46869  stoweidlem56  46871  stoweidlem59  46874  stoweidlem60  46875  fourier2  47042  qndenserrnbllem  47109  qndenserrn  47114  sge0rpcpnf  47236  hoidmvval0b  47405  hoiqssbllem3  47439  tmachlem-exagreecover  47761  imasetpreimafvbijlemfv1  48290  nfermltl8rev  48645  nfermltl2rev  48646  nfermltlrev  48647  isubgredg  48769  gpg5edgnedg  49033  nn0mnd  49081  opncldeqv  49815  opnneilv  49822  setrec1lem3  50602  dfrals2  50706