Definition df-rex 3062

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 3053). (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 3061	. 2 wff ∃𝑥 ∈ 𝐴 𝜑
5	2	cv 1541	. . . . 5 class 𝑥
6	5, 3	wcel 2114	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wex 1781	. 2 wff ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 206	1 wff (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  ralnex  3063  rexex  3067  rextru  3068  reximi2  3070  rexbii2  3080  rexlimiva  3130  reximdv2  3147  rexbidv2  3157  r19.41v  3167  r3ex  3176  reeanlem  3208  risset  3212  cbvrexvw  3216  rspe  3227  r19.23t  3233  r19.41  3241  reximd2a  3247  rexbida  3249  nfre1  3262  rexcom4  3264  r19.12  3286  rexeq  3293  rexeqfOLD  3328  reu5  3353  rmo5  3369  rexv  3469  2gencl  3484  3gencl  3485  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  4103  rexun  4149  reuun2  4278  reuss2  4279  reupick  4282  reupick3  4283  euelss  4285  reximdva0  4308  n0rex  4310  n0el  4317  inn0f  4324  r19.2z  4453  rexsns  4629  exsnrex  4638  dfuni2  4866  eluni2  4868  elunirab  4879  iuncom4  4956  iunxiun  5053  axrep6  5234  axrep6OLD  5235  axsepgfromrep  5240  intexrab  5293  opeliunxp  5692  opeliun2xp  5693  xpiundi  5696  xpiundir  5697  ssrelrn  5844  dmuni  5864  rnmpt  5907  elrnmpt1  5910  dfima2  6022  dfima3  6023  elima2  6026  dfco2a  6205  imaco  6210  elsnxp  6250  dfpo2  6255  fvelima2  6887  dffo4  7050  dffo5  7051  abrexco  7192  isomin  7285  imaeqsexvOLD  7311  imaeqexov  7598  zfrep6  7901  opabex3d  7911  opabex3rd  7912  opabex3  7913  abexssex  7916  abexex  7917  frxp  8070  dfrecs3  8306  rdglim2  8365  oarec  8491  oeeu  8533  mapsnd  8828  mapsnend  8977  pssnn  9097  enfii  9114  enp1i  9183  unblem2  9197  pwfir  9221  dffi2  9330  marypha2lem4  9345  marypha2  9346  zfregcl  9503  zfregclOLD  9504  axinf2  9553  zfinf2  9555  brttrcl2  9627  ttrclselem2  9639  rankuni  9779  scott0  9802  cp  9807  bnd2  9809  infpwfien  9976  aceq1  10031  dfac5lem2  10038  dfac5lem3  10039  dfac2b  10045  kmlem3  10067  kmlem6  10070  kmlem8  10072  kmlem14  10078  infmap2  10131  ackbij2  10156  cfub  10163  cfval2  10174  cflim3  10176  cfss  10179  cfslb  10180  isf32lem9  10275  zorn2lem6  10415  iundom2g  10454  winalim2  10611  grothprim  10749  genpass  10924  nqpr  10929  1idpr  10944  ltexprlem4  10954  ltexprlem5  10955  reclem2pr  10963  axrrecex  11078  dedekind  11300  sup2  12102  infm3  12105  nnunb  12401  2rexuz  12817  nnwos  12832  xrsupsslem  13226  xrinfmsslem  13227  hashgt23el  14351  ishashinf  14390  wwlktovfo  14885  maxprmfct  16640  vdwapun  16906  vdwmc  16910  vdwmc2  16911  ram0  16954  imasleval  17466  mreexexlem2d  17572  dfiso2  17700  isssc  17748  drsdirfi  18232  dirge  18530  pwmnd  18866  psgnunilem4  19430  odcau  19537  ablfac2  20024  lspprat  21112  lidlnz  21201  isbasis2g  22896  tgval2  22904  ntreq0  23025  neitr  23128  cmpfi  23356  is1stc2  23390  2ndcsb  23397  2ndcsep  23407  1stcelcls  23409  hausmapdom  23448  isfbas2  23783  fbssint  23786  isfil2  23804  elfg  23819  fgcl  23826  uffix2  23872  alexsubALTlem4  23998  lpbl  24451  metustexhalf  24504  metuel2  24513  restmetu  24518  bcthlem5  25288  lrrecfr  27943  upgrex  29169  uvtx01vtx  29474  uhgrvd00  29612  wlkswwlksf1o  29956  wwlksnextsurj  29977  frcond3  30348  frgr3vlem2  30353  3vfriswmgrlem  30356  frgrncvvdeqlem9  30386  ubthlem1  30949  axhcompl-zf  31077  isch3  31320  shne0i  31527  cnlnssadj  32159  reuxfrdf  32568  rexunirn  32569  rmoxfrd  32570  dmrab  32574  abrexdomjm  32585  abrexexd  32587  iunrnmptss  32643  ac6mapd  32704  1stpreimas  32787  fpwrelmapffslem  32813  qsxpid  33445  krull  33562  zarclsint  34031  ordtconnlem1  34083  ddemeas  34395  omssubaddlem  34458  omssubadd  34459  eulerpartlemgvv  34535  tgoldbachgt  34822  bnj168  34888  bnj956  34934  bnj1098  34941  bnj1143  34948  bnj1146  34949  bnj1185  34951  bnj1196  34952  bnj600  35077  bnj849  35083  bnj906  35088  bnj916  35091  bnj983  35109  bnj984  35110  bnj1083  35136  bnj1176  35163  bnj1186  35165  bnj1189  35167  bnj1228  35169  bnj1253  35175  bnj1398  35192  bnj1463  35213  bnj1312  35216  bnj1514  35221  exdifsn  35237  r1filimi  35261  axregszf  35287  onvf1odlem1  35299  onvf1odlem2  35300  wevgblacfn  35305  lfuhgr3  35316  cusgredgex  35318  loop1cycl  35333  erdszelem10  35396  ptpconn  35429  rexxfr3dALT  35835  coep  35948  coepr  35949  dffr5  35950  opelco3  35971  dfon2lem8  35984  brimg  36131  dfrecs2  36146  dfrdg4  36147  ellines  36348  cbvrexvw2  36423  neifg  36567  regsfromunir1  36672  bj-rexvw  37083  bj-gabima  37143  bj-snglc  37172  bj-snglss  37173  bj-rest10  37295  bj-restn0  37297  bj-restpw  37299  bj-rest0  37300  bj-restb  37301  bj-restuni  37304  bj-dfmpoa  37325  bj-finsumval0  37492  rnmptsn  37542  f1omptsnlem  37543  mptsnunlem  37545  topdifinffinlem  37554  isbasisrelowllem1  37562  isbasisrelowllem2  37563  relowlpssretop  37571  fvineqsneq  37619  pibt2  37624  poimirlem30  37853  abrexdom  37933  prdstotbnd  37997  elrnres  38481  eldmqsres2  38497  exanres  38504  rncnvepres  38512  rnxrnres  38625  1cossres  38722  eldm1cossres  38753  eldmqs1cossres  38947  disjlem17  39105  disjdmqscossss  39109  prtlem17  39204  prter2  39209  islshpat  39345  lsat0cv  39361  lshpsmreu  39437  atex  39734  islpln5  39863  islvol5  39907  pmapglb  40098  pmapglb2N  40099  pmapglb2xN  40100  elpaddn0  40128  pmapjat1  40181  polval2N  40234  osumcllem11N  40294  pexmidlem8N  40305  cdlemftr3  40893  dibelval3  41475  dibglbN  41494  dicelval3  41508  dihglbcpreN  41628  dihglb2  41670  dihjatcclem4  41749  mapdrvallem2  41973  mapdpglem3  42003  hdmapglem7a  42255  sticksstones3  42470  imaopab  42555  sn-sup2  42813  fimgmcyc  42856  prjspeclsp  42922  uniel  43526  nnoeomeqom  43621  tfsconcatlem  43645  tfsconcatrn  43651  tfsconcat0i  43654  rp-isfinite5  43825  rp-isfinite6  43826  minregex  43842  elintima  43961  iunrelexpuztr  44027  cotrclrcl  44050  neik0pk1imk0  44355  ntrneineine0lem  44391  ntrneineine1lem  44392  ntrneiel2  44394  cpcolld  44566  expandrexn  44599  ismnuprim  44602  rr-grothprimbi  44603  rr-groth  44607  ismnushort  44609  rr-grothshortbi  44611  rexbidar  44753  onfrALTlem5  44850  onfrALTlem2  44854  onfrALTlem1  44856  onfrALTlem5VD  45192  onfrALTlem2VD  45196  onfrALTlem1VD  45197  chordthmALT  45240  rspesbcd  45245  modelaxreplem3  45288  ssclaxsep  45290  permaxrep  45314  nregmodel  45325  rspcegf  45335  cncmpmax  45344  rfcnnnub  45348  nssrex  45397  eluni2f  45414  eliin2f  45415  suprnmpt  45485  founiiun0  45501  disjinfi  45503  ssfiunibd  45624  infrpge  45663  fsumiunss  45888  islpcn  45950  lptre2pt  45951  stoweidlem14  46325  stoweidlem34  46345  stoweidlem35  46346  stoweidlem43  46354  stoweidlem44  46355  stoweidlem50  46361  stoweidlem54  46365  stoweidlem56  46367  stoweidlem59  46370  stoweidlem60  46371  fourier2  46538  qndenserrnbllem  46605  qndenserrn  46610  sge0rpcpnf  46732  hoidmvval0b  46901  hoiqssbllem3  46935  chnsubseqword  47189  imasetpreimafvbijlemfv1  47716  nfermltl8rev  48055  nfermltl2rev  48056  nfermltlrev  48057  isubgredg  48179  gpg5edgnedg  48443  nn0mnd  48492  opncldeqv  49214  opnneilv  49221  setrec1lem3  50001