Definition df-rex 3070

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 3069). (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 3065	. 2 wff ∃𝑥 ∈ 𝐴 𝜑
5	2	cv 1538	. . . . 5 class 𝑥
6	5, 3	wcel 2106	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 396	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wex 1782	. 2 wff ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 205	1 wff (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  ralnex  3167  rexex  3171  reximi2  3175  rexbii2  3179  risset  3194  reximdv2  3199  rexbidv2  3224  rexcom4  3233  rspe  3237  nfre1  3239  reximd2a  3245  r19.23t  3246  rexbida  3251  ralrexbidOLD  3256  r19.12  3257  r19.12OLD  3258  r19.41v  3276  r19.41  3277  rexcomOLD  3285  reeanlem  3292  rexeqf  3333  reu5  3361  rmo5  3365  cbvrexvw  3384  cbvrexdva2  3393  rexv  3457  2gencl  3472  3gencl  3473  rspce  3550  ceqsrexv  3585  rexabOLD  3632  rexab2  3636  rexrab2  3637  morex  3654  reu2  3660  reu6  3661  reu3  3662  2reuswap  3681  2reuswap2  3682  2reu5lem3  3692  2reu5  3693  2rmoswap  3696  ssrexf  3985  rexdifi  4080  rexun  4124  reuun2  4248  reuss2  4249  reupick  4252  reupick3  4253  euelss  4255  reximdva0  4285  n0rex  4288  n0el  4295  r19.2z  4425  r19.2zb  4426  rexsns  4605  exsnrex  4616  dfuni2  4841  eluni2  4843  elunirab  4855  iuncom4  4932  iunxiun  5026  axrep6  5216  axsepgfromrep  5221  intexrab  5264  opeliunxp  5654  xpiundi  5657  xpiundir  5658  ssrelrn  5803  dmuni  5823  rnmpt  5864  elrnmpt1  5867  dfima2  5971  dfima3  5972  elima2  5975  dfco2a  6150  imaco  6155  elsnxp  6194  dfpo2  6199  dffo4  6979  dffo5  6980  abrexco  7117  isomin  7208  zfrep6  7797  opabex3d  7808  opabex3rd  7809  opabex3  7810  abexssex  7813  abexex  7814  frxp  7967  dfrecs3  8203  dfrecs3OLD  8204  rdglim2  8263  oarec  8393  oeeu  8434  mapsnd  8674  mapsnend  8826  pssnn  8951  pwfir  8959  enfii  8972  pssnnOLD  9040  unblem2  9067  dffi2  9182  marypha2lem4  9197  marypha2  9198  zfregcl  9353  axinf2  9398  zfinf2  9400  brttrcl2  9472  ttrclselem2  9484  rankuni  9621  scott0  9644  cp  9649  bnd2  9651  infpwfien  9818  aceq1  9873  dfac5lem2  9880  dfac5lem3  9881  dfac2b  9886  kmlem3  9908  kmlem6  9911  kmlem8  9913  kmlem14  9919  infmap2  9974  ackbij2  9999  cfub  10005  cfval2  10016  cflim3  10018  cfss  10021  cfslb  10022  isf32lem9  10117  zorn2lem6  10257  iundom2g  10296  winalim2  10452  grothprim  10590  genpass  10765  nqpr  10770  1idpr  10785  ltexprlem4  10795  ltexprlem5  10796  reclem2pr  10804  axrrecex  10919  dedekind  11138  sup2  11931  infm3  11934  nnunb  12229  2rexuz  12640  nnwos  12655  xrsupsslem  13041  xrinfmsslem  13042  hashgt23el  14139  ishashinf  14177  cshwsexa  14537  wwlktovfo  14673  maxprmfct  16414  vdwapun  16675  vdwmc  16679  vdwmc2  16680  ram0  16723  imasleval  17252  mreexexlem2d  17354  dfiso2  17484  isssc  17532  drsdirfi  18023  dirge  18321  pwmnd  18576  psgnunilem4  19105  odcau  19209  ablfac2  19692  lspprat  20415  lidlnz  20499  isbasis2g  22098  tgval2  22106  ntreq0  22228  neitr  22331  cmpfi  22559  is1stc2  22593  2ndcsb  22600  2ndcsep  22610  1stcelcls  22612  hausmapdom  22651  isfbas2  22986  fbssint  22989  isfil2  23007  elfg  23022  fgcl  23029  uffix2  23075  alexsubALTlem4  23201  lpbl  23659  metustexhalf  23712  metuel2  23721  restmetu  23726  bcthlem5  24492  upgrex  27462  uvtx01vtx  27764  uhgrvd00  27901  wlkswwlksf1o  28244  wwlksnextsurj  28265  frcond3  28633  frgr3vlem2  28638  3vfriswmgrlem  28641  frgrncvvdeqlem9  28671  ubthlem1  29232  axhcompl-zf  29360  isch3  29603  shne0i  29810  cnlnssadj  30442  reuxfrdf  30839  rexunirn  30840  rmoxfrd  30841  dmrab  30844  abrexdomjm  30852  abrexexd  30854  iunrnmptss  30905  1stpreimas  31038  fpwrelmapffslem  31067  qsxpid  31558  krull  31643  zarclsint  31822  ordtconnlem1  31874  ddemeas  32204  omssubaddlem  32266  omssubadd  32267  eulerpartlemgvv  32343  tgoldbachgt  32643  bnj168  32709  bnj956  32756  bnj1098  32763  bnj1143  32770  bnj1146  32771  bnj1185  32773  bnj1196  32774  bnj600  32899  bnj849  32905  bnj906  32910  bnj916  32913  bnj983  32931  bnj984  32932  bnj1083  32958  bnj1176  32985  bnj1186  32987  bnj1189  32989  bnj1228  32991  bnj1253  32997  bnj1398  33014  bnj1463  33035  bnj1312  33038  bnj1514  33043  exdifsn  33053  lfuhgr3  33081  cusgredgex  33083  loop1cycl  33099  erdszelem10  33162  ptpconn  33195  imaeqsexv  33690  coep  33719  coepr  33720  dffr5  33721  opelco3  33749  dfon2lem8  33766  lrrecfr  34100  brimg  34239  dfrecs2  34252  dfrdg4  34253  ellines  34454  neifg  34560  bj-rexvw  35065  bj-gabima  35128  bj-snglc  35159  bj-snglss  35160  bj-rest10  35259  bj-restn0  35261  bj-restpw  35263  bj-rest0  35264  bj-restb  35265  bj-restuni  35268  bj-dfmpoa  35289  bj-finsumval0  35456  rnmptsn  35506  f1omptsnlem  35507  mptsnunlem  35509  topdifinffinlem  35518  isbasisrelowllem1  35526  isbasisrelowllem2  35527  relowlpssretop  35535  fvineqsneq  35583  pibt2  35588  poimirlem30  35807  abrexdom  35888  prdstotbnd  35952  eldmqsres2  36422  exanres  36430  rncnvepres  36439  rnxrnres  36525  1cossres  36552  eldm1cossres  36578  eldmqs1cossres  36771  prtlem17  36890  prter2  36895  islshpat  37031  lsat0cv  37047  lshpsmreu  37123  atex  37420  islpln5  37549  islvol5  37593  pmapglb  37784  pmapglb2N  37785  pmapglb2xN  37786  elpaddn0  37814  pmapjat1  37867  polval2N  37920  osumcllem11N  37980  pexmidlem8N  37991  cdlemftr3  38579  dibelval3  39161  dibglbN  39180  dicelval3  39194  dihglbcpreN  39314  dihglb2  39356  dihjatcclem4  39435  mapdordlem2  39651  mapdrvallem2  39659  mapdpglem3  39689  hdmapglem7a  39941  sticksstones3  40104  imaopab  40207  sn-sup2  40439  prjspeclsp  40451  rp-isfinite5  41124  rp-isfinite6  41125  minregex  41141  elintima  41261  iunrelexpuztr  41327  cotrclrcl  41350  neik0pk1imk0  41657  ntrneineine0lem  41693  ntrneineine1lem  41694  ntrneiel2  41696  cpcolld  41876  expandrexn  41909  ismnuprim  41912  rr-grothprimbi  41913  rr-groth  41917  ismnushort  41919  rr-grothshortbi  41921  rexbidar  42064  onfrALTlem5  42162  onfrALTlem2  42166  onfrALTlem1  42168  onfrALTlem5VD  42505  onfrALTlem2VD  42509  onfrALTlem1VD  42510  chordthmALT  42553  rspcegf  42566  cncmpmax  42575  rfcnnnub  42579  inn0f  42621  nssrex  42636  eluni2f  42653  eliin2f  42654  suprnmpt  42710  founiiun0  42728  disjinfi  42731  fvelima2  42806  ssfiunibd  42848  infrpge  42890  fsumiunss  43116  islpcn  43180  lptre2pt  43181  stoweidlem14  43555  stoweidlem34  43575  stoweidlem35  43576  stoweidlem43  43584  stoweidlem44  43585  stoweidlem50  43591  stoweidlem54  43595  stoweidlem56  43597  stoweidlem59  43600  stoweidlem60  43601  fourier2  43768  qndenserrnbllem  43835  qndenserrn  43840  sge0rpcpnf  43959  hoidmvval0b  44128  hoiqssbllem3  44162  imasetpreimafvbijlemfv1  44855  nfermltl8rev  45194  nfermltl2rev  45195  nfermltlrev  45196  nn0mnd  45373  opeliun2xp  45668  rextru  46149  opncldeqv  46195  opnneilv  46202  setrec1lem3  46395