Definition df-rex 3089

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 3079). (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 3088	. 2 wff ∃𝑥 ∈ 𝐴 𝜑
5	2	cv 1561	. . . . 5 class 𝑥
6	5, 3	wcel 2144	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 399	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wex 1801	. 2 wff ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 208	1 wff (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  ralnex  3090  rexex  3094  rextru  3095  reximi2  3097  rexbii2  3107  rexlimiva  3157  reximdv2  3174  rexbidv2  3184  r19.41v  3194  r3ex  3203  reeanlem  3235  risset  3239  cbvrexvw  3243  rspe  3254  r19.23t  3260  r19.41  3268  reximd2a  3274  rexbida  3276  nfre1  3289  rexcom4  3291  r19.12  3313  rexeq  3318  reu5  3371  rmo5  3387  rexv  3483  2gencl  3498  3gencl  3499  rspce  3572  ceqsrexv  3616  rexab2  3664  rexrab2  3665  morex  3684  reu2  3690  reu6  3691  reu3  3692  2reuswap  3711  2reuswap2  3712  2reu5lem3  3722  2reu5  3723  2rmoswap  3726  nssrex  4003  ssrexf  4005  ssrexv  4008  rexss  4012  rexdifi  4105  rexun  4150  reuun2  4279  reuss2  4280  reupick  4283  reupick3  4284  euelss  4286  reximdva0  4310  n0rex  4312  n0el  4319  inn0f  4326  r19.2z  4455  rexsns  4632  exsnrex  4641  dfuni2  4869  eluni2  4871  elunirab  4882  iuncom4  4960  iunxiun  5056  axrep6  5238  axrep6OLD  5239  replem  5240  axsepgfromrep  5246  intexrab  5305  opeliunxp  5716  opeliun2xp  5717  xpiundi  5720  xpiundir  5721  ssrelrn  5872  dmuni  5892  rnmpt  5935  elrnmpt1  5938  dfima2  6053  dfima3  6054  elima2  6057  dfco2a  6235  imaco  6240  elsnxp  6280  dfpo2  6285  fvelima2  6921  dffo4  7086  dffo5  7087  abrexco  7230  isomin  7323  imaeqsexvOLD  7349  imaeqexov  7636  zfrep6OLD  7938  opabex3d  7948  opabex3rd  7949  opabex3  7950  abexssex  7953  abexex  7954  frxp  8108  dfrecs3  8345  rdglim2  8405  oarec  8533  oeeu  8575  mapsnd  8870  mapsnend  9019  pssnn  9139  enfii  9156  enp1i  9225  unblem2  9239  pwfir  9263  dffi2  9371  marypha2lem4  9386  marypha2  9387  zfregcl  9544  zfregclOLD  9545  axinf2  9597  zfinf2  9599  brttrcl2  9671  ttrclselem2  9683  rankuni  9823  scott0  9846  cp  9851  bnd2  9853  infpwfien  10020  aceq1  10075  dfac5lem2  10082  dfac5lem3  10083  dfac2b  10089  kmlem3  10111  kmlem6  10114  kmlem8  10116  kmlem14  10122  infmap2  10175  ackbij2  10200  cfub  10207  cfval2  10219  cflim3  10221  cfss  10224  cfslb  10225  isf32lem9  10320  zorn2lem6  10460  iundom2g  10499  winalim2  10656  grothprim  10794  genpass  10969  nqpr  10974  1idpr  10989  ltexprlem4  10999  ltexprlem5  11000  reclem2pr  11008  axrrecex  11123  dedekind  11348  sup2  12150  infm3  12153  nnunb  12479  2rexuz  12903  nnwos  12918  xrsupsslem  13312  xrinfmsslem  13313  hashgt23el  14439  ishashinf  14478  wwlktovfo  14973  maxprmfct  16746  vdwapun  17012  vdwmc  17016  vdwmc2  17017  ram0  17060  imasleval  17573  mreexexlem2d  17679  dfiso2  17807  isssc  17855  drsdirfi  18339  dirge  18637  pwmnd  18976  psgnunilem4  19539  odcau  19646  ablfac2  20133  lspprat  21225  lidlnz  21314  isbasis2g  23010  tgval2  23018  ntreq0  23139  neitr  23242  cmpfi  23470  is1stc2  23504  2ndcsb  23511  2ndcsep  23521  1stcelcls  23523  hausmapdom  23562  isfbas2  23897  fbssint  23900  isfil2  23918  elfg  23933  fgcl  23940  uffix2  23986  alexsubALTlem4  24112  lpbl  24565  metustexhalf  24618  metuel2  24627  restmetu  24632  bcthlem5  25392  lrrecfr  28038  upgrex  29295  uvtx01vtx  29600  uhgrvd00  29737  wlkswwlksf1o  30081  wwlksnextsurj  30102  frcond3  30473  frgr3vlem2  30478  3vfriswmgrlem  30481  frgrncvvdeqlem9  30511  ubthlem1  31075  axhcompl-zf  31203  isch3  31446  shne0i  31653  cnlnssadj  32285  reuxfrdf  32692  rexunirn  32693  rmoxfrd  32694  dmrab  32698  abrexdomjm  32708  abrexexd  32710  iunrnmptss  32767  ac6mapd  32827  1stpreimas  32910  fpwrelmapffslem  32936  qsxpid  33550  krull  33669  zarclsint  34171  ordtconnlem1  34223  ddemeas  34535  omssubaddlem  34598  omssubadd  34599  eulerpartlemgvv  34675  tgoldbachgt  34959  bnj168  35028  bnj956  35074  bnj1098  35081  bnj1143  35087  bnj1146  35088  bnj1185  35090  bnj1196  35091  bnj600  35216  bnj849  35222  bnj906  35227  bnj916  35230  bnj983  35248  bnj984  35249  bnj1083  35275  bnj1176  35302  bnj1186  35304  bnj1189  35306  bnj1228  35308  bnj1253  35314  bnj1398  35331  bnj1463  35352  bnj1312  35355  bnj1514  35360  exdifsn  35376  r1filimi  35403  axprALT2  35409  axregszf  35429  onvf1odlem1  35450  onvf1odlem2  35451  wevgblacfn  35458  lfuhgr3  35475  cusgredgex  35477  loop1cycl  35492  erdszelem10  35555  ptpconn  35588  rexxfr3dALT  35994  coep  36107  coepr  36108  dffr5  36109  opelco3  36130  dfon2lem8  36143  brimg  36290  dfrecs2  36305  dfrdg4  36306  ellines  36507  cbvrexvw2  36592  neifg  36736  regsfromunir1  36905  bj-rexvw  37370  bj-gabima  37430  bj-snglc  37459  bj-snglss  37460  bj-axseprep  37564  bj-axreprepsep  37565  bj-rest10  37583  bj-restn0  37585  bj-restpw  37587  bj-rest0  37588  bj-restb  37589  bj-restuni  37592  bj-dfmpoa  37613  bj-finsumval0  37782  rnmptsn  37834  f1omptsnlem  37835  mptsnunlem  37837  topdifinffinlem  37846  isbasisrelowllem1  37854  isbasisrelowllem2  37855  relowlpssretop  37863  fvineqsneq  37911  pibt2  37916  poimirlem30  38154  abrexdom  38234  prdstotbnd  38298  elrnres  38782  eldmqsres2  38798  exanres  38805  rncnvepres  38813  rnxrnres  38926  1cossres  39023  eldm1cossres  39054  eldmqs1cossres  39248  disjlem17  39406  disjdmqscossss  39410  prtlem17  39505  prter2  39510  islshpat  39646  lsat0cv  39662  lshpsmreu  39738  atex  40035  islpln5  40164  islvol5  40208  pmapglb  40399  pmapglb2N  40400  pmapglb2xN  40401  elpaddn0  40429  pmapjat1  40482  polval2N  40535  osumcllem11N  40595  pexmidlem8N  40606  cdlemftr3  41194  dibelval3  41776  dibglbN  41795  dicelval3  41809  dihglbcpreN  41929  dihglb2  41971  dihjatcclem4  42050  mapdrvallem2  42274  mapdpglem3  42304  hdmapglem7a  42556  sticksstones3  42770  imaopab  42855  sn-sup2  43118  fimgmcyc  43157  prjspeclsp  43199  uniel  43799  nnoeomeqom  43894  tfsconcatlem  43918  tfsconcatrn  43924  tfsconcat0i  43927  rp-isfinite5  44098  rp-isfinite6  44099  minregex  44115  elintima  44234  iunrelexpuztr  44300  cotrclrcl  44323  neik0pk1imk0  44628  ntrneineine0lem  44664  ntrneineine1lem  44665  ntrneiel2  44667  cpcolld  44839  expandrexn  44872  ismnuprim  44875  rr-grothprimbi  44876  rr-groth  44880  ismnushort  44882  rr-grothshortbi  44884  rexbidar  45026  onfrALTlem5  45123  onfrALTlem2  45127  onfrALTlem1  45129  onfrALTlem5VD  45465  onfrALTlem2VD  45469  onfrALTlem1VD  45470  chordthmALT  45513  rspesbcd  45518  modelaxreplem3  45561  ssclaxsep  45563  permaxrep  45587  nregmodel  45598  rspcegf  45608  cncmpmax  45617  rfcnnnub  45621  eluni2f  45686  eliin2f  45687  suprnmpt  45757  founiiun0  45773  disjinfi  45775  ssfiunibd  45893  infrpge  45932  fsumiunss  46156  islpcn  46218  lptre2pt  46219  stoweidlem14  46593  stoweidlem34  46613  stoweidlem35  46614  stoweidlem43  46622  stoweidlem44  46623  stoweidlem50  46629  stoweidlem54  46633  stoweidlem56  46635  stoweidlem59  46638  stoweidlem60  46639  fourier2  46806  qndenserrnbllem  46873  qndenserrn  46878  sge0rpcpnf  47000  hoidmvval0b  47169  hoiqssbllem3  47203  chnsubseqword  47459  imasetpreimafvbijlemfv1  48014  nfermltl8rev  48369  nfermltl2rev  48370  nfermltlrev  48371  isubgredg  48493  gpg5edgnedg  48757  nn0mnd  48806  opncldeqv  49528  opnneilv  49535  setrec1lem3  50315