Definition df-rex 3054

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

This definition is referenced by:  ralnex  3055  rexex  3059  rextru  3060  reximi2  3062  rexbii2  3072  rexlimiva  3126  reximdv2  3143  rexbidv2  3153  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  3288  rexeq  3295  cbvrexdva2OLD  3323  rexeqfOLD  3331  reu5  3356  rmo5  3374  rexv  3475  2gencl  3490  3gencl  3491  rspce  3577  ceqsrexv  3621  rexab2  3670  rexrab2  3671  morex  3690  reu2  3696  reu6  3697  reu3  3698  2reuswap  3717  2reuswap2  3718  2reu5lem3  3728  2reu5  3729  2rmoswap  3732  ssrexf  4013  ssrexv  4016  rexss  4022  rexdifi  4113  rexun  4159  reuun2  4288  reuss2  4289  reupick  4292  reupick3  4293  euelss  4295  reximdva0  4318  n0rex  4320  n0el  4327  inn0f  4334  r19.2z  4458  r19.2zb  4459  rexsns  4635  exsnrex  4644  dfuni2  4873  eluni2  4875  elunirab  4886  iuncom4  4964  iunxiun  5061  axrep6  5243  axrep6OLD  5244  axsepgfromrep  5249  intexrab  5302  opeliunxp  5705  opeliun2xp  5706  xpiundi  5709  xpiundir  5710  ssrelrn  5858  dmuni  5878  rnmpt  5921  elrnmpt1  5924  dfima2  6033  dfima3  6034  elima2  6037  dfco2a  6219  imaco  6224  elsnxp  6264  dfpo2  6269  fvelima2  6913  dffo4  7075  dffo5  7076  abrexco  7218  isomin  7312  imaeqsexvOLD  7338  imaeqexov  7627  zfrep6  7933  opabex3d  7944  opabex3rd  7945  opabex3  7946  abexssex  7949  abexex  7950  frxp  8105  dfrecs3  8341  rdglim2  8400  oarec  8526  oeeu  8567  mapsnd  8859  mapsnend  9007  pssnn  9132  enfii  9150  enp1i  9224  unblem2  9240  pwfir  9266  dffi2  9374  marypha2lem4  9389  marypha2  9390  zfregcl  9547  axinf2  9593  zfinf2  9595  brttrcl2  9667  ttrclselem2  9679  rankuni  9816  scott0  9839  cp  9844  bnd2  9846  infpwfien  10015  aceq1  10070  dfac5lem2  10077  dfac5lem3  10078  dfac2b  10084  kmlem3  10106  kmlem6  10109  kmlem8  10111  kmlem14  10117  infmap2  10170  ackbij2  10195  cfub  10202  cfval2  10213  cflim3  10215  cfss  10218  cfslb  10219  isf32lem9  10314  zorn2lem6  10454  iundom2g  10493  winalim2  10649  grothprim  10787  genpass  10962  nqpr  10967  1idpr  10982  ltexprlem4  10992  ltexprlem5  10993  reclem2pr  11001  axrrecex  11116  dedekind  11337  sup2  12139  infm3  12142  nnunb  12438  2rexuz  12859  nnwos  12874  xrsupsslem  13267  xrinfmsslem  13268  hashgt23el  14389  ishashinf  14428  cshwsexaOLD  14790  wwlktovfo  14924  maxprmfct  16679  vdwapun  16945  vdwmc  16949  vdwmc2  16950  ram0  16993  imasleval  17504  mreexexlem2d  17606  dfiso2  17734  isssc  17782  drsdirfi  18266  dirge  18562  pwmnd  18864  psgnunilem4  19427  odcau  19534  ablfac2  20021  lspprat  21063  lidlnz  21152  isbasis2g  22835  tgval2  22843  ntreq0  22964  neitr  23067  cmpfi  23295  is1stc2  23329  2ndcsb  23336  2ndcsep  23346  1stcelcls  23348  hausmapdom  23387  isfbas2  23722  fbssint  23725  isfil2  23743  elfg  23758  fgcl  23765  uffix2  23811  alexsubALTlem4  23937  lpbl  24391  metustexhalf  24444  metuel2  24453  restmetu  24458  bcthlem5  25228  lrrecfr  27850  upgrex  29019  uvtx01vtx  29324  uhgrvd00  29462  wlkswwlksf1o  29809  wwlksnextsurj  29830  frcond3  30198  frgr3vlem2  30203  3vfriswmgrlem  30206  frgrncvvdeqlem9  30236  ubthlem1  30799  axhcompl-zf  30927  isch3  31170  shne0i  31377  cnlnssadj  32009  reuxfrdf  32420  rexunirn  32421  rmoxfrd  32422  dmrab  32426  abrexdomjm  32436  abrexexd  32438  iunrnmptss  32494  ac6mapd  32549  1stpreimas  32629  fpwrelmapffslem  32655  qsxpid  33333  krull  33450  zarclsint  33862  ordtconnlem1  33914  ddemeas  34226  omssubaddlem  34290  omssubadd  34291  eulerpartlemgvv  34367  tgoldbachgt  34654  bnj168  34720  bnj956  34766  bnj1098  34773  bnj1143  34780  bnj1146  34781  bnj1185  34783  bnj1196  34784  bnj600  34909  bnj849  34915  bnj906  34920  bnj916  34923  bnj983  34941  bnj984  34942  bnj1083  34968  bnj1176  34995  bnj1186  34997  bnj1189  34999  bnj1228  35001  bnj1253  35007  bnj1398  35024  bnj1463  35045  bnj1312  35048  bnj1514  35053  exdifsn  35069  onvf1odlem1  35090  onvf1odlem2  35091  wevgblacfn  35096  lfuhgr3  35107  cusgredgex  35109  loop1cycl  35124  erdszelem10  35187  ptpconn  35220  rexxfr3dALT  35626  coep  35739  coepr  35740  dffr5  35741  opelco3  35762  dfon2lem8  35778  brimg  35925  dfrecs2  35938  dfrdg4  35939  ellines  36140  cbvrexvw2  36215  neifg  36359  bj-rexvw  36868  bj-gabima  36928  bj-snglc  36957  bj-snglss  36958  bj-rest10  37076  bj-restn0  37078  bj-restpw  37080  bj-rest0  37081  bj-restb  37082  bj-restuni  37085  bj-dfmpoa  37106  bj-finsumval0  37273  rnmptsn  37323  f1omptsnlem  37324  mptsnunlem  37326  topdifinffinlem  37335  isbasisrelowllem1  37343  isbasisrelowllem2  37344  relowlpssretop  37352  fvineqsneq  37400  pibt2  37405  poimirlem30  37644  abrexdom  37724  prdstotbnd  37788  elrnres  38260  eldmqsres2  38276  exanres  38283  rncnvepres  38291  rnxrnres  38385  1cossres  38420  eldm1cossres  38451  eldmqs1cossres  38651  disjlem17  38791  disjdmqscossss  38795  prtlem17  38869  prter2  38874  islshpat  39010  lsat0cv  39026  lshpsmreu  39102  atex  39400  islpln5  39529  islvol5  39573  pmapglb  39764  pmapglb2N  39765  pmapglb2xN  39766  elpaddn0  39794  pmapjat1  39847  polval2N  39900  osumcllem11N  39960  pexmidlem8N  39971  cdlemftr3  40559  dibelval3  41141  dibglbN  41160  dicelval3  41174  dihglbcpreN  41294  dihglb2  41336  dihjatcclem4  41415  mapdordlem2  41631  mapdrvallem2  41639  mapdpglem3  41669  hdmapglem7a  41921  sticksstones3  42136  imaopab  42219  sn-sup2  42479  fimgmcyc  42522  prjspeclsp  42600  uniel  43206  nnoeomeqom  43301  tfsconcatlem  43325  tfsconcatrn  43331  tfsconcat0i  43334  rp-isfinite5  43506  rp-isfinite6  43507  minregex  43523  elintima  43642  iunrelexpuztr  43708  cotrclrcl  43731  neik0pk1imk0  44036  ntrneineine0lem  44072  ntrneineine1lem  44073  ntrneiel2  44075  cpcolld  44247  expandrexn  44280  ismnuprim  44283  rr-grothprimbi  44284  rr-groth  44288  ismnushort  44290  rr-grothshortbi  44292  rexbidar  44435  onfrALTlem5  44532  onfrALTlem2  44536  onfrALTlem1  44538  onfrALTlem5VD  44874  onfrALTlem2VD  44878  onfrALTlem1VD  44879  chordthmALT  44922  rspesbcd  44927  modelaxreplem3  44970  ssclaxsep  44972  permaxrep  44996  nregmodel  45007  rspcegf  45017  cncmpmax  45026  rfcnnnub  45030  nssrex  45080  eluni2f  45097  eliin2f  45098  suprnmpt  45168  founiiun0  45184  disjinfi  45186  ssfiunibd  45307  infrpge  45347  fsumiunss  45573  islpcn  45637  lptre2pt  45638  stoweidlem14  46012  stoweidlem34  46032  stoweidlem35  46033  stoweidlem43  46041  stoweidlem44  46042  stoweidlem50  46048  stoweidlem54  46052  stoweidlem56  46054  stoweidlem59  46057  stoweidlem60  46058  fourier2  46225  qndenserrnbllem  46292  qndenserrn  46297  sge0rpcpnf  46419  hoidmvval0b  46588  hoiqssbllem3  46622  imasetpreimafvbijlemfv1  47404  nfermltl8rev  47743  nfermltl2rev  47744  nfermltlrev  47745  isubgredg  47866  nn0mnd  48167  opncldeqv  48890  opnneilv  48897  setrec1lem3  49678