Definition df-rex 3077

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 3068). (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 3076	. 2 wff ∃𝑥 ∈ 𝐴 𝜑
5	2	cv 1536	. . . . 5 class 𝑥
6	5, 3	wcel 2108	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wex 1777	. 2 wff ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 206	1 wff (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  ralnex  3078  rexex  3082  rextru  3083  reximi2  3085  rexbii2  3096  ralrexbidOLD  3113  rexlimiva  3153  reximdv2  3170  rexbidv2  3181  r19.41v  3195  r3ex  3204  reeanlem  3234  risset  3239  cbvrexvw  3244  rspe  3255  r19.23t  3261  r19.41  3269  reximd2a  3275  rexbida  3278  nfre1  3291  rexcom4  3294  rexcomOLD  3297  r19.12  3320  r19.12OLD  3321  rexeq  3330  cbvrexdva2OLD  3358  rexeqfOLD  3363  reu5  3390  rmo5  3408  rexv  3517  2gencl  3534  3gencl  3535  rspce  3624  ceqsrexv  3668  rexabOLD  3717  rexab2  3721  rexrab2  3722  morex  3741  reu2  3747  reu6  3748  reu3  3749  2reuswap  3768  2reuswap2  3769  2reu5lem3  3779  2reu5  3780  2rmoswap  3783  ssrexf  4075  ssrexv  4078  rexdifi  4173  rexun  4219  reuun2  4344  reuss2  4345  reupick  4348  reupick3  4349  euelss  4351  reximdva0  4378  n0rex  4380  n0el  4387  inn0f  4394  r19.2z  4518  r19.2zb  4519  rexsns  4693  exsnrex  4704  dfuni2  4933  eluni2  4935  elunirab  4946  iuncom4  5023  iunxiun  5120  axrep6  5310  axsepgfromrep  5315  intexrab  5365  opeliunxp  5767  xpiundi  5770  xpiundir  5771  ssrelrn  5919  dmuni  5939  rnmpt  5980  elrnmpt1  5983  dfima2  6091  dfima3  6092  elima2  6095  dfco2a  6277  imaco  6282  elsnxp  6322  dfpo2  6327  dffo4  7137  dffo5  7138  abrexco  7281  isomin  7373  imaeqsexvOLD  7399  imaeqexov  7688  zfrep6  7995  opabex3d  8006  opabex3rd  8007  opabex3  8008  abexssex  8011  abexex  8012  frxp  8167  dfrecs3  8428  dfrecs3OLD  8429  rdglim2  8488  oarec  8618  oeeu  8659  mapsnd  8944  mapsnend  9101  pssnn  9234  enfii  9252  enp1i  9341  unblem2  9357  pwfir  9383  dffi2  9492  marypha2lem4  9507  marypha2  9508  zfregcl  9663  axinf2  9709  zfinf2  9711  brttrcl2  9783  ttrclselem2  9795  rankuni  9932  scott0  9955  cp  9960  bnd2  9962  infpwfien  10131  aceq1  10186  dfac5lem2  10193  dfac5lem3  10194  dfac2b  10200  kmlem3  10222  kmlem6  10225  kmlem8  10227  kmlem14  10233  infmap2  10286  ackbij2  10311  cfub  10318  cfval2  10329  cflim3  10331  cfss  10334  cfslb  10335  isf32lem9  10430  zorn2lem6  10570  iundom2g  10609  winalim2  10765  grothprim  10903  genpass  11078  nqpr  11083  1idpr  11098  ltexprlem4  11108  ltexprlem5  11109  reclem2pr  11117  axrrecex  11232  dedekind  11453  sup2  12251  infm3  12254  nnunb  12549  2rexuz  12965  nnwos  12980  xrsupsslem  13369  xrinfmsslem  13370  hashgt23el  14473  ishashinf  14512  cshwsexaOLD  14873  wwlktovfo  15007  maxprmfct  16756  vdwapun  17021  vdwmc  17025  vdwmc2  17026  ram0  17069  imasleval  17601  mreexexlem2d  17703  dfiso2  17833  isssc  17881  drsdirfi  18375  dirge  18673  pwmnd  18972  psgnunilem4  19539  odcau  19646  ablfac2  20133  lspprat  21178  lidlnz  21275  isbasis2g  22976  tgval2  22984  ntreq0  23106  neitr  23209  cmpfi  23437  is1stc2  23471  2ndcsb  23478  2ndcsep  23488  1stcelcls  23490  hausmapdom  23529  isfbas2  23864  fbssint  23867  isfil2  23885  elfg  23900  fgcl  23907  uffix2  23953  alexsubALTlem4  24079  lpbl  24537  metustexhalf  24590  metuel2  24599  restmetu  24604  bcthlem5  25381  lrrecfr  27994  upgrex  29127  uvtx01vtx  29432  uhgrvd00  29570  wlkswwlksf1o  29912  wwlksnextsurj  29933  frcond3  30301  frgr3vlem2  30306  3vfriswmgrlem  30309  frgrncvvdeqlem9  30339  ubthlem1  30902  axhcompl-zf  31030  isch3  31273  shne0i  31480  cnlnssadj  32112  reuxfrdf  32519  rexunirn  32520  rmoxfrd  32521  dmrab  32525  abrexdomjm  32535  abrexexd  32537  iunrnmptss  32588  1stpreimas  32717  fpwrelmapffslem  32746  qsxpid  33355  krull  33472  zarclsint  33818  ordtconnlem1  33870  ddemeas  34200  omssubaddlem  34264  omssubadd  34265  eulerpartlemgvv  34341  tgoldbachgt  34640  bnj168  34706  bnj956  34752  bnj1098  34759  bnj1143  34766  bnj1146  34767  bnj1185  34769  bnj1196  34770  bnj600  34895  bnj849  34901  bnj906  34906  bnj916  34909  bnj983  34927  bnj984  34928  bnj1083  34954  bnj1176  34981  bnj1186  34983  bnj1189  34985  bnj1228  34987  bnj1253  34993  bnj1398  35010  bnj1463  35031  bnj1312  35034  bnj1514  35039  exdifsn  35055  wevgblacfn  35076  lfuhgr3  35087  cusgredgex  35089  loop1cycl  35105  erdszelem10  35168  ptpconn  35201  rexxfr3dALT  35607  coep  35714  coepr  35715  dffr5  35716  opelco3  35738  dfon2lem8  35754  brimg  35901  dfrecs2  35914  dfrdg4  35915  ellines  36116  cbvrexvw2  36193  neifg  36337  bj-rexvw  36846  bj-gabima  36906  bj-snglc  36935  bj-snglss  36936  bj-rest10  37054  bj-restn0  37056  bj-restpw  37058  bj-rest0  37059  bj-restb  37060  bj-restuni  37063  bj-dfmpoa  37084  bj-finsumval0  37251  rnmptsn  37301  f1omptsnlem  37302  mptsnunlem  37304  topdifinffinlem  37313  isbasisrelowllem1  37321  isbasisrelowllem2  37322  relowlpssretop  37330  fvineqsneq  37378  pibt2  37383  poimirlem30  37610  abrexdom  37690  prdstotbnd  37754  elrnres  38227  eldmqsres2  38244  exanres  38251  rncnvepres  38259  rnxrnres  38355  1cossres  38385  eldm1cossres  38416  eldmqs1cossres  38615  disjlem17  38755  disjdmqscossss  38759  prtlem17  38832  prter2  38837  islshpat  38973  lsat0cv  38989  lshpsmreu  39065  atex  39363  islpln5  39492  islvol5  39536  pmapglb  39727  pmapglb2N  39728  pmapglb2xN  39729  elpaddn0  39757  pmapjat1  39810  polval2N  39863  osumcllem11N  39923  pexmidlem8N  39934  cdlemftr3  40522  dibelval3  41104  dibglbN  41123  dicelval3  41137  dihglbcpreN  41257  dihglb2  41299  dihjatcclem4  41378  mapdordlem2  41594  mapdrvallem2  41602  mapdpglem3  41632  hdmapglem7a  41884  sticksstones3  42105  imaopab  42224  sn-sup2  42447  fimgmcyc  42489  prjspeclsp  42567  uniel  43178  nnoeomeqom  43274  tfsconcatlem  43298  tfsconcatrn  43304  tfsconcat0i  43307  rp-isfinite5  43479  rp-isfinite6  43480  minregex  43496  elintima  43615  iunrelexpuztr  43681  cotrclrcl  43704  neik0pk1imk0  44009  ntrneineine0lem  44045  ntrneineine1lem  44046  ntrneiel2  44048  cpcolld  44227  expandrexn  44260  ismnuprim  44263  rr-grothprimbi  44264  rr-groth  44268  ismnushort  44270  rr-grothshortbi  44272  rexbidar  44415  onfrALTlem5  44513  onfrALTlem2  44517  onfrALTlem1  44519  onfrALTlem5VD  44856  onfrALTlem2VD  44860  onfrALTlem1VD  44861  chordthmALT  44904  rspcegf  44923  cncmpmax  44932  rfcnnnub  44936  nssrex  44988  eluni2f  45005  eliin2f  45006  suprnmpt  45081  founiiun0  45097  disjinfi  45099  fvelima2  45169  ssfiunibd  45224  infrpge  45266  fsumiunss  45496  islpcn  45560  lptre2pt  45561  stoweidlem14  45935  stoweidlem34  45955  stoweidlem35  45956  stoweidlem43  45964  stoweidlem44  45965  stoweidlem50  45971  stoweidlem54  45975  stoweidlem56  45977  stoweidlem59  45980  stoweidlem60  45981  fourier2  46148  qndenserrnbllem  46215  qndenserrn  46220  sge0rpcpnf  46342  hoidmvval0b  46511  hoiqssbllem3  46545  imasetpreimafvbijlemfv1  47277  nfermltl8rev  47616  nfermltl2rev  47617  nfermltlrev  47618  nn0mnd  47902  opeliun2xp  48057  opncldeqv  48581  opnneilv  48588  setrec1lem3  48781