Definition df-rex 3072

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 3063). (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 3071	. 2 wff ∃𝑥 ∈ 𝐴 𝜑
5	2	cv 1541	. . . . 5 class 𝑥
6	5, 3	wcel 2107	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 397	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wex 1782	. 2 wff ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 205	1 wff (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  ralnex  3073  rexex  3077  rextru  3078  reximi2  3080  rexbii2  3091  ralrexbidOLD  3108  rexlimiva  3148  reximdv2  3165  rexbidv2  3175  r19.41v  3189  reeanlem  3226  risset  3231  cbvrexvw  3236  rspe  3247  r19.23t  3253  r19.41  3261  reximd2a  3267  rexbida  3270  nfre1  3283  rexcom4  3286  rexcomOLD  3289  r19.12  3312  r19.12OLD  3313  rexeq  3322  cbvrexdva2OLD  3347  rexeqfOLD  3352  reu5  3379  rmo5  3397  rexv  3500  2gencl  3517  3gencl  3518  rspce  3602  ceqsrexv  3644  rexabOLD  3692  rexab2  3696  rexrab2  3697  morex  3716  reu2  3722  reu6  3723  reu3  3724  2reuswap  3743  2reuswap2  3744  2reu5lem3  3754  2reu5  3755  2rmoswap  3758  ssrexf  4049  rexdifi  4146  rexun  4191  reuun2  4315  reuss2  4316  reupick  4319  reupick3  4320  euelss  4322  reximdva0  4352  n0rex  4355  n0el  4362  r19.2z  4495  r19.2zb  4496  rexsns  4674  exsnrex  4685  dfuni2  4911  eluni2  4913  elunirab  4925  iuncom4  5006  iunxiun  5101  axrep6  5293  axsepgfromrep  5298  intexrab  5341  opeliunxp  5744  xpiundi  5747  xpiundir  5748  ssrelrn  5895  dmuni  5915  rnmpt  5955  elrnmpt1  5958  dfima2  6062  dfima3  6063  elima2  6066  dfco2a  6246  imaco  6251  elsnxp  6291  dfpo2  6296  dffo4  7105  dffo5  7106  abrexco  7243  isomin  7334  imaeqsexv  7360  imaeqexov  7645  zfrep6  7941  opabex3d  7952  opabex3rd  7953  opabex3  7954  abexssex  7957  abexex  7958  frxp  8112  dfrecs3  8372  dfrecs3OLD  8373  rdglim2  8432  oarec  8562  oeeu  8603  mapsnd  8880  mapsnend  9036  pssnn  9168  pwfir  9176  enfii  9189  pssnnOLD  9265  enp1i  9279  unblem2  9296  dffi2  9418  marypha2lem4  9433  marypha2  9434  zfregcl  9589  axinf2  9635  zfinf2  9637  brttrcl2  9709  ttrclselem2  9721  rankuni  9858  scott0  9881  cp  9886  bnd2  9888  infpwfien  10057  aceq1  10112  dfac5lem2  10119  dfac5lem3  10120  dfac2b  10125  kmlem3  10147  kmlem6  10150  kmlem8  10152  kmlem14  10158  infmap2  10213  ackbij2  10238  cfub  10244  cfval2  10255  cflim3  10257  cfss  10260  cfslb  10261  isf32lem9  10356  zorn2lem6  10496  iundom2g  10535  winalim2  10691  grothprim  10829  genpass  11004  nqpr  11009  1idpr  11024  ltexprlem4  11034  ltexprlem5  11035  reclem2pr  11043  axrrecex  11158  dedekind  11377  sup2  12170  infm3  12173  nnunb  12468  2rexuz  12884  nnwos  12899  xrsupsslem  13286  xrinfmsslem  13287  hashgt23el  14384  ishashinf  14424  cshwsexaOLD  14775  wwlktovfo  14909  maxprmfct  16646  vdwapun  16907  vdwmc  16911  vdwmc2  16912  ram0  16955  imasleval  17487  mreexexlem2d  17589  dfiso2  17719  isssc  17767  drsdirfi  18258  dirge  18556  pwmnd  18818  psgnunilem4  19365  odcau  19472  ablfac2  19959  lspprat  20766  lidlnz  20853  isbasis2g  22451  tgval2  22459  ntreq0  22581  neitr  22684  cmpfi  22912  is1stc2  22946  2ndcsb  22953  2ndcsep  22963  1stcelcls  22965  hausmapdom  23004  isfbas2  23339  fbssint  23342  isfil2  23360  elfg  23375  fgcl  23382  uffix2  23428  alexsubALTlem4  23554  lpbl  24012  metustexhalf  24065  metuel2  24074  restmetu  24079  bcthlem5  24845  lrrecfr  27429  upgrex  28383  uvtx01vtx  28685  uhgrvd00  28822  wlkswwlksf1o  29164  wwlksnextsurj  29185  frcond3  29553  frgr3vlem2  29558  3vfriswmgrlem  29561  frgrncvvdeqlem9  29591  ubthlem1  30154  axhcompl-zf  30282  isch3  30525  shne0i  30732  cnlnssadj  31364  reuxfrdf  31762  rexunirn  31763  rmoxfrd  31764  dmrab  31768  abrexdomjm  31775  abrexexd  31777  iunrnmptss  31828  1stpreimas  31958  fpwrelmapffslem  31988  qsxpid  32505  krull  32625  zarclsint  32883  ordtconnlem1  32935  ddemeas  33265  omssubaddlem  33329  omssubadd  33330  eulerpartlemgvv  33406  tgoldbachgt  33706  bnj168  33772  bnj956  33818  bnj1098  33825  bnj1143  33832  bnj1146  33833  bnj1185  33835  bnj1196  33836  bnj600  33961  bnj849  33967  bnj906  33972  bnj916  33975  bnj983  33993  bnj984  33994  bnj1083  34020  bnj1176  34047  bnj1186  34049  bnj1189  34051  bnj1228  34053  bnj1253  34059  bnj1398  34076  bnj1463  34097  bnj1312  34100  bnj1514  34105  exdifsn  34115  lfuhgr3  34141  cusgredgex  34143  loop1cycl  34159  erdszelem10  34222  ptpconn  34255  coep  34753  coepr  34754  dffr5  34755  opelco3  34777  dfon2lem8  34793  brimg  34940  dfrecs2  34953  dfrdg4  34954  ellines  35155  neifg  35304  bj-rexvw  35808  bj-gabima  35868  bj-snglc  35898  bj-snglss  35899  bj-rest10  36017  bj-restn0  36019  bj-restpw  36021  bj-rest0  36022  bj-restb  36023  bj-restuni  36026  bj-dfmpoa  36047  bj-finsumval0  36214  rnmptsn  36264  f1omptsnlem  36265  mptsnunlem  36267  topdifinffinlem  36276  isbasisrelowllem1  36284  isbasisrelowllem2  36285  relowlpssretop  36293  fvineqsneq  36341  pibt2  36346  poimirlem30  36566  abrexdom  36646  prdstotbnd  36710  elrnres  37187  eldmqsres2  37204  exanres  37212  rncnvepres  37220  rnxrnres  37317  1cossres  37347  eldm1cossres  37378  eldmqs1cossres  37577  disjlem17  37717  disjdmqscossss  37721  prtlem17  37794  prter2  37799  islshpat  37935  lsat0cv  37951  lshpsmreu  38027  atex  38325  islpln5  38454  islvol5  38498  pmapglb  38689  pmapglb2N  38690  pmapglb2xN  38691  elpaddn0  38719  pmapjat1  38772  polval2N  38825  osumcllem11N  38885  pexmidlem8N  38896  cdlemftr3  39484  dibelval3  40066  dibglbN  40085  dicelval3  40099  dihglbcpreN  40219  dihglb2  40261  dihjatcclem4  40340  mapdordlem2  40556  mapdrvallem2  40564  mapdpglem3  40594  hdmapglem7a  40846  sticksstones3  41012  imaopab  41098  sn-sup2  41390  prjspeclsp  41402  uniel  42014  nnoeomeqom  42110  tfsconcatlem  42134  tfsconcatrn  42140  tfsconcat0i  42143  rp-isfinite5  42316  rp-isfinite6  42317  minregex  42333  elintima  42452  iunrelexpuztr  42518  cotrclrcl  42541  neik0pk1imk0  42846  ntrneineine0lem  42882  ntrneineine1lem  42883  ntrneiel2  42885  cpcolld  43065  expandrexn  43098  ismnuprim  43101  rr-grothprimbi  43102  rr-groth  43106  ismnushort  43108  rr-grothshortbi  43110  rexbidar  43253  onfrALTlem5  43351  onfrALTlem2  43355  onfrALTlem1  43357  onfrALTlem5VD  43694  onfrALTlem2VD  43698  onfrALTlem1VD  43699  chordthmALT  43742  rspcegf  43755  cncmpmax  43764  rfcnnnub  43768  inn0f  43808  nssrex  43823  eluni2f  43840  eliin2f  43841  suprnmpt  43918  founiiun0  43936  disjinfi  43939  fvelima2  44012  ssfiunibd  44067  infrpge  44109  fsumiunss  44339  islpcn  44403  lptre2pt  44404  stoweidlem14  44778  stoweidlem34  44798  stoweidlem35  44799  stoweidlem43  44807  stoweidlem44  44808  stoweidlem50  44814  stoweidlem54  44818  stoweidlem56  44820  stoweidlem59  44823  stoweidlem60  44824  fourier2  44991  qndenserrnbllem  45058  qndenserrn  45063  sge0rpcpnf  45185  hoidmvval0b  45354  hoiqssbllem3  45388  imasetpreimafvbijlemfv1  46119  nfermltl8rev  46458  nfermltl2rev  46459  nfermltlrev  46460  nn0mnd  46637  opeliun2xp  47056  opncldeqv  47582  opnneilv  47589  setrec1lem3  47782