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 1568	. . . . 5 class 𝑥
6	5, 3	wcel 2142	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 400	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wex 1808	. 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  3318  reu5  3370  rmo5  3386  rexv  3481  2gencl  3496  3gencl  3497  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  5316  opeliunxp  5727  opeliun2xp  5728  xpiundi  5731  xpiundir  5732  ssrelrn  5883  dmuni  5903  rnmpt  5946  elrnmpt1  5949  dfima2  6063  dfima3  6064  elima2  6067  dfco2a  6246  imaco  6251  elsnxp  6292  dfpo2  6297  fvelima2  6933  dffo4  7098  dffo5  7099  abrexco  7242  isomin  7335  imaeqsexvOLD  7363  imaeqexov  7650  zfrep6OLD  7950  opabex3d  7960  opabex3rd  7961  opabex3  7962  abexssex  7965  abexex  7966  frxp  8120  dfrecs3  8357  rdglim2  8417  oarec  8545  oeeu  8587  mapsnd  8882  mapsnend  9031  pssnn  9151  enfii  9168  enp1i  9237  unblem2  9251  pwfir  9274  dffi2  9381  marypha2lem4  9396  marypha2  9397  zfregcl  9554  zfregclOLD  9555  axinf2  9607  zfinf2  9609  brttrcl2  9681  ttrclselem2  9693  rankuni  9833  scott0b  9864  scott0OLD  9865  cp  9881  bnd2  9883  infpwfien  10053  aceq1  10108  dfac5lem2  10115  dfac5lem3  10116  dfac2b  10121  kmlem3  10143  kmlem6  10146  kmlem8  10148  kmlem14  10154  infmap2  10207  ackbij2  10232  cfub  10238  cfval2  10250  cflim3  10252  cfss  10255  cfslb  10256  isf32lem9  10351  zorn2lem6  10491  iundom2g  10530  winalim2  10687  grothprim  10825  genpass  11000  nqpr  11005  1idpr  11020  ltexprlem4  11030  ltexprlem5  11031  reclem2pr  11039  axrrecex  11154  dedekind  11379  sup2  12177  infm3  12180  nnunb  12506  2rexuz  12930  nnwos  12945  xrsupsslem  13339  xrinfmsslem  13340  hashgt23el  14468  ishashinf  14507  wwlktovfo  15002  maxprmfct  16774  vdwapun  17040  vdwmc  17044  vdwmc2  17045  ram0  17088  imasleval  17601  mreexexlem2d  17707  dfiso2  17835  isssc  17883  drsdirfi  18367  dirge  18665  pwmnd  19005  qsxpid  19249  psgnunilem4  19573  odcau  19680  ablfac2  20167  lspprat  21288  lidlnz  21387  isbasis2g  23116  tgval2  23124  ntreq0  23245  neitr  23348  cmpfi  23576  is1stc2  23610  2ndcsb  23617  2ndcsep  23627  1stcelcls  23629  hausmapdom  23668  isfbas2  24003  fbssint  24006  isfil2  24024  elfg  24039  fgcl  24046  uffix2  24092  alexsubALTlem4  24218  lpbl  24671  metustexhalf  24724  metuel2  24733  restmetu  24738  bcthlem5  25498  lrrecfr  28147  upgrex  29453  uvtx01vtx  29758  uhgrvd00  29895  wlkswwlksf1o  30239  wwlksnextsurj  30260  frcond3  30631  frgr3vlem2  30636  3vfriswmgrlem  30639  frgrncvvdeqlem9  30669  ubthlem1  31233  axhcompl-zf  31361  isch3  31604  shne0i  31811  cnlnssadj  32443  reuxfrdf  32848  rexunirn  32849  rmoxfrd  32850  dmrab  32854  abrexdomjm  32864  abrexexd  32866  iunrnmptss  32921  ac6mapd  32979  1stpreimas  33062  fpwrelmapffslem  33088  krull  33770  zarclsint  34271  ordtconnlem1  34323  ddemeas  34635  omssubaddlem  34698  omssubadd  34699  eulerpartlemgvv  34775  tgoldbachgt  35059  bnj168  35128  bnj956  35174  bnj1098  35181  bnj1143  35187  bnj1146  35188  bnj1185  35190  bnj1196  35191  bnj600  35316  bnj849  35322  bnj906  35327  bnj916  35330  bnj983  35348  bnj984  35349  bnj1083  35375  bnj1176  35402  bnj1186  35404  bnj1189  35406  bnj1228  35408  bnj1253  35414  bnj1398  35431  bnj1463  35452  bnj1312  35455  bnj1514  35460  exdifsn  35477  r1filimi  35506  axprALT2  35512  axregszf  35550  karddom  35582  kardsdom  35583  kardfi  35591  onvf1odlem1  35595  onvf1odlem2  35596  wevgblacfn  35603  lfuhgr3  35620  cusgredgex  35622  loop1cycl  35637  erdszelem10  35700  ptpconn  35733  rexxfr3dALT  36139  coep  36252  coepr  36253  dffr5  36254  opelco3  36275  dfon2lem8  36288  brimg  36435  dfrecs2  36450  dfrdg4  36451  ellines  36652  cbvrexvw2  36767  neifg  36910  regsfromunir1  37079  bj-rexvw  37543  bj-gabima  37604  bj-snglc  37633  bj-snglss  37634  bj-axseprep  37739  bj-axreprepsep  37740  bj-rest10  37758  bj-restn0  37760  bj-restpw  37762  bj-rest0  37763  bj-restb  37764  bj-restuni  37767  bj-dfmpoa  37788  bj-finsumval0  37957  rnmptsn  38009  f1omptsnlem  38010  mptsnunlem  38012  topdifinffinlem  38021  isbasisrelowllem1  38029  isbasisrelowllem2  38030  relowlpssretop  38038  fvineqsneq  38086  pibt2  38091  poimirlem30  38329  abrexdom  38409  prdstotbnd  38473  elrnres  38955  eldmqsres2  38971  exanres  38978  rncnvepres  38986  rnxrnres  39099  1cossres  39196  eldm1cossres  39227  eldmqs1cossres  39421  disjlem17  39579  disjdmqscossss  39583  prtlem17  39678  prter2  39683  islshpat  39819  lsat0cv  39835  lshpsmreu  39911  atex  40208  islpln5  40337  islvol5  40381  pmapglb  40572  pmapglb2N  40573  pmapglb2xN  40574  elpaddn0  40602  pmapjat1  40655  polval2N  40708  osumcllem11N  40768  pexmidlem8N  40779  cdlemftr3  41367  dibelval3  41949  dibglbN  41968  dicelval3  41982  dihglbcpreN  42102  dihglb2  42144  dihjatcclem4  42223  mapdrvallem2  42447  mapdpglem3  42477  hdmapglem7a  42729  sticksstones3  42943  imaopab  43030  sn-sup2  43293  fimgmcyc  43330  prjspeclsp  43372  uniel  43972  nnoeomeqom  44067  tfsconcatlem  44091  tfsconcatrn  44097  tfsconcat0i  44100  rp-isfinite5  44271  rp-isfinite6  44272  minregex  44288  elintima  44407  iunrelexpuztr  44473  cotrclrcl  44496  neik0pk1imk0  44801  ntrneineine0lem  44837  ntrneineine1lem  44838  ntrneiel2  44840  cpcolld  44996  expandrexn  45029  ismnuprim  45032  rr-grothprimbi  45033  rr-groth  45037  ismnushort  45039  rr-grothshortbi  45041  rexbidar  45183  onfrALTlem5  45279  onfrALTlem2  45283  onfrALTlem1  45285  onfrALTlem5VD  45621  onfrALTlem2VD  45625  onfrALTlem1VD  45626  chordthmALT  45669  rspesbcd  45674  modelaxreplem3  45717  ssclaxsep  45719  permaxrep  45743  nregmodel  45754  rspcegf  45771  cncmpmax  45780  rfcnnnub  45784  eluni2f  45849  eliin2f  45850  suprnmpt  45920  founiiun0  45936  disjinfi  45938  ssfiunibd  46056  infrpge  46095  fsumiunss  46319  islpcn  46381  lptre2pt  46382  stoweidlem14  46756  stoweidlem34  46776  stoweidlem35  46777  stoweidlem43  46785  stoweidlem44  46786  stoweidlem50  46792  stoweidlem54  46796  stoweidlem56  46798  stoweidlem59  46801  stoweidlem60  46802  fourier2  46969  qndenserrnbllem  47036  qndenserrn  47041  sge0rpcpnf  47163  hoidmvval0b  47332  hoiqssbllem3  47366  chnsubseqword  47622  imasetpreimafvbijlemfv1  48180  nfermltl8rev  48535  nfermltl2rev  48536  nfermltlrev  48537  isubgredg  48659  gpg5edgnedg  48923  nn0mnd  48972  opncldeqv  49708  opnneilv  49715  setrec1lem3  50495  dfrals2  50596