Definition df-rex 3112

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 3111). (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 3107	. 2 wff ∃𝑥 ∈ 𝐴 𝜑
5	2	cv 1537	. . . . 5 class 𝑥
6	5, 3	wcel 2111	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 399	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wex 1781	. 2 wff ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 209	1 wff (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  ralnex  3199  rexex  3203  reximi2  3207  rexbii2  3208  rexcom4  3212  risset  3226  reximdv2  3230  rexbidv2  3254  rspe  3263  nfre1  3265  reximd2a  3271  r19.23t  3272  rexbida  3277  ralrexbid  3281  r19.12  3283  r19.41v  3300  r19.41  3301  rexcom  3308  reeanlem  3318  rexeqf  3351  reu5  3375  rmo5  3379  cbvrexvw  3397  cbvrexdva2  3404  cbvrexdva2OLD  3405  rexv  3467  2gencl  3482  3gencl  3483  rspce  3560  ceqsrexv  3597  rexab  3634  rexab2  3639  rexab2OLD  3640  rexrab2  3641  morex  3658  reu2  3664  reu6  3665  reu3  3666  2reuswap  3685  2reuswap2  3686  2reu5lem3  3696  2reu5  3697  2rmoswap  3700  ssrexf  3979  rexdifi  4073  rexun  4117  reuss2  4235  reuun2  4238  reupick  4239  reupick3  4240  euelss  4242  reximdva0  4265  n0rex  4268  n0el  4275  r19.2z  4398  r19.2zb  4399  rexsns  4569  exsnrex  4578  dfuni2  4802  eluni2  4804  elunirab  4816  iuncom4  4889  iunxiun  4982  axrep6  5161  axsepgfromrep  5165  intexrab  5207  opeliunxp  5583  xpiundi  5586  xpiundir  5587  ssrelrn  5727  dmuni  5747  rnmpt  5791  elrnmpt1  5794  dfima2  5898  dfima3  5899  elima2  5902  dfco2a  6066  imaco  6071  elsnxp  6110  dffo4  6846  dffo5  6847  abrexco  6981  isomin  7069  zfrep6  7638  opabex3d  7648  opabex3rd  7649  opabex3  7650  abexssex  7653  abexex  7654  frxp  7803  dfrecs3  7992  rdglim2  8051  oarec  8171  oeeu  8212  mapsnd  8433  mapsnend  8571  pssnn  8720  unblem2  8755  dffi2  8871  marypha2lem4  8886  marypha2  8887  zfregcl  9042  axinf2  9087  zfinf2  9089  rankuni  9276  scott0  9299  cp  9304  bnd2  9306  infpwfien  9473  aceq1  9528  dfac5lem2  9535  dfac5lem3  9536  dfac2b  9541  kmlem3  9563  kmlem6  9566  kmlem8  9568  kmlem14  9574  infmap2  9629  ackbij2  9654  cfub  9660  cfval2  9671  cflim3  9673  cfss  9676  cfslb  9677  isf32lem9  9772  zorn2lem6  9912  iundom2g  9951  winalim2  10107  grothprim  10245  genpass  10420  nqpr  10425  1idpr  10440  ltexprlem4  10450  ltexprlem5  10451  reclem2pr  10459  axrrecex  10574  dedekind  10792  sup2  11584  infm3  11587  nnunb  11881  2rexuz  12288  nnwos  12303  xrsupsslem  12688  xrinfmsslem  12689  hashgt23el  13781  ishashinf  13817  cshwsexa  14177  wwlktovfo  14313  maxprmfct  16043  vdwapun  16300  vdwmc  16304  vdwmc2  16305  ram0  16348  imasleval  16806  mreexexlem2d  16908  dfiso2  17034  isssc  17082  drsdirfi  17540  dirge  17839  pwmnd  18094  psgnunilem4  18617  odcau  18721  ablfac2  19204  lspprat  19918  lidlnz  19994  isbasis2g  21553  tgval2  21561  ntreq0  21682  neitr  21785  cmpfi  22013  is1stc2  22047  2ndcsb  22054  2ndcsep  22064  1stcelcls  22066  hausmapdom  22105  isfbas2  22440  fbssint  22443  isfil2  22461  elfg  22476  fgcl  22483  uffix2  22529  alexsubALTlem4  22655  lpbl  23110  metustexhalf  23163  metuel2  23172  restmetu  23177  bcthlem5  23932  upgrex  26885  uvtx01vtx  27187  uhgrvd00  27324  wlkswwlksf1o  27665  wwlksnextsurj  27686  frcond3  28054  frgr3vlem2  28059  3vfriswmgrlem  28062  frgrncvvdeqlem9  28092  ubthlem1  28653  axhcompl-zf  28781  isch3  29024  shne0i  29231  cnlnssadj  29863  reuxfrdf  30262  rexunirn  30263  rmoxfrd  30264  dmrab  30267  abrexdomjm  30275  abrexexd  30277  iunrnmptss  30329  1stpreimas  30465  fpwrelmapffslem  30494  qsxpid  30978  krull  31051  zarclsint  31225  ordtconnlem1  31277  ddemeas  31605  omssubaddlem  31667  omssubadd  31668  eulerpartlemgvv  31744  tgoldbachgt  32044  bnj168  32110  bnj956  32158  bnj1098  32165  bnj1143  32172  bnj1146  32173  bnj1185  32175  bnj1196  32176  bnj600  32301  bnj849  32307  bnj906  32312  bnj916  32315  bnj983  32333  bnj984  32334  bnj1083  32360  bnj1176  32387  bnj1186  32389  bnj1189  32391  bnj1228  32393  bnj1253  32399  bnj1398  32416  bnj1463  32437  bnj1312  32440  bnj1514  32445  exdifsn  32455  lfuhgr3  32479  cusgredgex  32481  loop1cycl  32497  erdszelem10  32560  ptpconn  32593  coep  33100  coepr  33101  dffr5  33102  dfpo2  33104  opelco3  33131  dfon2lem8  33148  brimg  33511  dfrecs2  33524  dfrdg4  33525  ellines  33726  neifg  33832  bj-rexvw  34320  bj-snglc  34405  bj-snglss  34406  bj-rest10  34503  bj-restn0  34505  bj-restpw  34507  bj-rest0  34508  bj-restb  34509  bj-restuni  34512  bj-dfmpoa  34533  bj-finsumval0  34700  rnmptsn  34752  f1omptsnlem  34753  mptsnunlem  34755  topdifinffinlem  34764  isbasisrelowllem1  34772  isbasisrelowllem2  34773  relowlpssretop  34781  fvineqsneq  34829  pibt2  34834  poimirlem30  35087  abrexdom  35168  prdstotbnd  35232  eldmqsres2  35704  exanres  35712  rncnvepres  35721  rnxrnres  35807  1cossres  35834  eldm1cossres  35860  eldmqs1cossres  36053  prtlem17  36172  prter2  36177  islshpat  36313  lsat0cv  36329  lshpsmreu  36405  atex  36702  islpln5  36831  islvol5  36875  pmapglb  37066  pmapglb2N  37067  pmapglb2xN  37068  elpaddn0  37096  pmapjat1  37149  polval2N  37202  osumcllem11N  37262  pexmidlem8N  37273  cdlemftr3  37861  dibelval3  38443  dibglbN  38462  dicelval3  38476  dihglbcpreN  38596  dihglb2  38638  dihjatcclem4  38717  mapdordlem2  38933  mapdrvallem2  38941  mapdpglem3  38971  hdmapglem7a  39223  imaopab  39413  sn-sup2  39594  prjspeclsp  39606  rp-isfinite5  40225  rp-isfinite6  40226  elintima  40354  iunrelexpuztr  40420  cotrclrcl  40443  neik0pk1imk0  40750  ntrneineine0lem  40786  ntrneineine1lem  40787  ntrneiel2  40789  cpcolld  40966  expandrexn  40999  ismnuprim  41002  rr-grothprimbi  41003  rr-groth  41007  rexbidar  41150  onfrALTlem5  41248  onfrALTlem2  41252  onfrALTlem1  41254  onfrALTlem5VD  41591  onfrALTlem2VD  41595  onfrALTlem1VD  41596  chordthmALT  41639  rspcegf  41652  cncmpmax  41661  rfcnnnub  41665  inn0f  41707  nssrex  41722  eluni2f  41739  eliin2f  41740  suprnmpt  41798  founiiun0  41817  disjinfi  41820  fvelima2  41898  ssfiunibd  41941  infrpge  41983  fsumiunss  42217  islpcn  42281  lptre2pt  42282  stoweidlem14  42656  stoweidlem34  42676  stoweidlem35  42677  stoweidlem43  42685  stoweidlem44  42686  stoweidlem50  42692  stoweidlem54  42696  stoweidlem56  42698  stoweidlem59  42701  stoweidlem60  42702  fourier2  42869  qndenserrnbllem  42936  qndenserrn  42941  sge0rpcpnf  43060  hoidmvval0b  43229  hoiqssbllem3  43263  imasetpreimafvbijlemfv1  43920  nfermltl8rev  44260  nfermltl2rev  44261  nfermltlrev  44262  nn0mnd  44439  opeliun2xp  44734  setrec1lem3  45219