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 1539	. . . . 5 class 𝑥
6	5, 3	wcel 2105	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 396	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wex 1780	. 2 wff ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 205	1 wff (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  ralnex  3073  rexex  3077  reximi2  3079  rexbii2  3090  ralrexbidOLD  3107  rexlimiva  3141  reximdv2  3158  rexbidv2  3168  r19.41v  3182  reeanlem  3213  risset  3218  cbvrexvw  3223  rspe  3229  r19.23t  3235  r19.41  3243  reximd2a  3249  rexbida  3252  nfre1  3265  rexcom4  3268  rexcomOLD  3271  r19.12  3294  r19.12OLD  3295  cbvrexdva2OLD  3322  rexeqf  3326  reu5  3352  rmo5  3370  rexv  3466  2gencl  3481  3gencl  3482  rspce  3559  ceqsrexv  3594  rexabOLD  3641  rexab2  3645  rexrab2  3646  morex  3663  reu2  3669  reu6  3670  reu3  3671  2reuswap  3690  2reuswap2  3691  2reu5lem3  3701  2reu5  3702  2rmoswap  3705  ssrexf  3994  rexdifi  4090  rexun  4134  reuun2  4258  reuss2  4259  reupick  4262  reupick3  4263  euelss  4265  reximdva0  4295  n0rex  4298  n0el  4305  r19.2z  4435  r19.2zb  4436  rexsns  4613  exsnrex  4624  dfuni2  4850  eluni2  4852  elunirab  4864  iuncom4  4943  iunxiun  5037  axrep6  5229  axsepgfromrep  5234  intexrab  5277  opeliunxp  5670  xpiundi  5673  xpiundir  5674  ssrelrn  5821  dmuni  5841  rnmpt  5881  elrnmpt1  5884  dfima2  5986  dfima3  5987  elima2  5990  dfco2a  6169  imaco  6174  elsnxp  6214  dfpo2  6219  dffo4  7016  dffo5  7017  abrexco  7154  isomin  7245  zfrep6  7840  opabex3d  7851  opabex3rd  7852  opabex3  7853  abexssex  7856  abexex  7857  frxp  8009  dfrecs3  8248  dfrecs3OLD  8249  rdglim2  8308  oarec  8439  oeeu  8480  mapsnd  8720  mapsnend  8876  pssnn  9008  pwfir  9016  enfii  9029  pssnnOLD  9105  enp1i  9119  unblem2  9135  dffi2  9250  marypha2lem4  9265  marypha2  9266  zfregcl  9421  axinf2  9466  zfinf2  9468  brttrcl2  9540  ttrclselem2  9552  rankuni  9689  scott0  9712  cp  9717  bnd2  9719  infpwfien  9888  aceq1  9943  dfac5lem2  9950  dfac5lem3  9951  dfac2b  9956  kmlem3  9978  kmlem6  9981  kmlem8  9983  kmlem14  9989  infmap2  10044  ackbij2  10069  cfub  10075  cfval2  10086  cflim3  10088  cfss  10091  cfslb  10092  isf32lem9  10187  zorn2lem6  10327  iundom2g  10366  winalim2  10522  grothprim  10660  genpass  10835  nqpr  10840  1idpr  10855  ltexprlem4  10865  ltexprlem5  10866  reclem2pr  10874  axrrecex  10989  dedekind  11208  sup2  12001  infm3  12004  nnunb  12299  2rexuz  12710  nnwos  12725  xrsupsslem  13111  xrinfmsslem  13112  hashgt23el  14208  ishashinf  14246  cshwsexa  14606  wwlktovfo  14742  maxprmfct  16481  vdwapun  16742  vdwmc  16746  vdwmc2  16747  ram0  16790  imasleval  17319  mreexexlem2d  17421  dfiso2  17551  isssc  17599  drsdirfi  18090  dirge  18388  pwmnd  18643  psgnunilem4  19172  odcau  19276  ablfac2  19759  lspprat  20486  lidlnz  20570  isbasis2g  22169  tgval2  22177  ntreq0  22299  neitr  22402  cmpfi  22630  is1stc2  22664  2ndcsb  22671  2ndcsep  22681  1stcelcls  22683  hausmapdom  22722  isfbas2  23057  fbssint  23060  isfil2  23078  elfg  23093  fgcl  23100  uffix2  23146  alexsubALTlem4  23272  lpbl  23730  metustexhalf  23783  metuel2  23792  restmetu  23797  bcthlem5  24563  upgrex  27570  uvtx01vtx  27872  uhgrvd00  28009  wlkswwlksf1o  28352  wwlksnextsurj  28373  frcond3  28741  frgr3vlem2  28746  3vfriswmgrlem  28749  frgrncvvdeqlem9  28779  ubthlem1  29340  axhcompl-zf  29468  isch3  29711  shne0i  29918  cnlnssadj  30550  reuxfrdf  30947  rexunirn  30948  rmoxfrd  30949  dmrab  30952  abrexdomjm  30960  abrexexd  30962  iunrnmptss  31013  1stpreimas  31146  fpwrelmapffslem  31175  qsxpid  31662  krull  31748  zarclsint  31928  ordtconnlem1  31980  ddemeas  32310  omssubaddlem  32372  omssubadd  32373  eulerpartlemgvv  32449  tgoldbachgt  32749  bnj168  32815  bnj956  32862  bnj1098  32869  bnj1143  32876  bnj1146  32877  bnj1185  32879  bnj1196  32880  bnj600  33005  bnj849  33011  bnj906  33016  bnj916  33019  bnj983  33037  bnj984  33038  bnj1083  33064  bnj1176  33091  bnj1186  33093  bnj1189  33095  bnj1228  33097  bnj1253  33103  bnj1398  33120  bnj1463  33141  bnj1312  33144  bnj1514  33149  exdifsn  33159  lfuhgr3  33187  cusgredgex  33189  loop1cycl  33205  erdszelem10  33268  ptpconn  33301  imaeqsexv  33794  coep  33822  coepr  33823  dffr5  33824  opelco3  33851  dfon2lem8  33868  lrrecfr  34161  brimg  34300  dfrecs2  34313  dfrdg4  34314  ellines  34515  neifg  34621  bj-rexvw  35125  bj-gabima  35188  bj-snglc  35219  bj-snglss  35220  bj-rest10  35319  bj-restn0  35321  bj-restpw  35323  bj-rest0  35324  bj-restb  35325  bj-restuni  35328  bj-dfmpoa  35349  bj-finsumval0  35516  rnmptsn  35566  f1omptsnlem  35567  mptsnunlem  35569  topdifinffinlem  35578  isbasisrelowllem1  35586  isbasisrelowllem2  35587  relowlpssretop  35595  fvineqsneq  35643  pibt2  35648  poimirlem30  35867  abrexdom  35948  prdstotbnd  36012  elrnres  36493  eldmqsres2  36510  exanres  36518  rncnvepres  36526  rnxrnres  36625  1cossres  36655  eldm1cossres  36686  eldmqs1cossres  36885  disjlem17  37025  disjdmqscossss  37029  prtlem17  37102  prter2  37107  islshpat  37243  lsat0cv  37259  lshpsmreu  37335  atex  37632  islpln5  37761  islvol5  37805  pmapglb  37996  pmapglb2N  37997  pmapglb2xN  37998  elpaddn0  38026  pmapjat1  38079  polval2N  38132  osumcllem11N  38192  pexmidlem8N  38203  cdlemftr3  38791  dibelval3  39373  dibglbN  39392  dicelval3  39406  dihglbcpreN  39526  dihglb2  39568  dihjatcclem4  39647  mapdordlem2  39863  mapdrvallem2  39871  mapdpglem3  39901  hdmapglem7a  40153  sticksstones3  40319  imaopab  40417  sn-sup2  40649  prjspeclsp  40661  rp-isfinite5  41352  rp-isfinite6  41353  minregex  41369  elintima  41489  iunrelexpuztr  41555  cotrclrcl  41578  neik0pk1imk0  41885  ntrneineine0lem  41921  ntrneineine1lem  41922  ntrneiel2  41924  cpcolld  42104  expandrexn  42137  ismnuprim  42140  rr-grothprimbi  42141  rr-groth  42145  ismnushort  42147  rr-grothshortbi  42149  rexbidar  42292  onfrALTlem5  42390  onfrALTlem2  42394  onfrALTlem1  42396  onfrALTlem5VD  42733  onfrALTlem2VD  42737  onfrALTlem1VD  42738  chordthmALT  42781  rspcegf  42794  cncmpmax  42803  rfcnnnub  42807  inn0f  42849  nssrex  42864  eluni2f  42881  eliin2f  42882  suprnmpt  42945  founiiun0  42963  disjinfi  42966  fvelima2  43042  ssfiunibd  43091  infrpge  43133  fsumiunss  43360  islpcn  43424  lptre2pt  43425  stoweidlem14  43799  stoweidlem34  43819  stoweidlem35  43820  stoweidlem43  43828  stoweidlem44  43829  stoweidlem50  43835  stoweidlem54  43839  stoweidlem56  43841  stoweidlem59  43844  stoweidlem60  43845  fourier2  44012  qndenserrnbllem  44079  qndenserrn  44084  sge0rpcpnf  44204  hoidmvval0b  44373  hoiqssbllem3  44407  imasetpreimafvbijlemfv1  45114  nfermltl8rev  45453  nfermltl2rev  45454  nfermltlrev  45455  nn0mnd  45632  opeliun2xp  45927  rextru  46408  opncldeqv  46454  opnneilv  46461  setrec1lem3  46654