Definition df-rex 3070

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 3069). (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 3065	. 2 wff ∃𝑥 ∈ 𝐴 𝜑
5	2	cv 1542	. . . . 5 class 𝑥
6	5, 3	wcel 2112	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 399	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wex 1787	. 2 wff ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 209	1 wff (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  ralnex  3164  rexex  3168  reximi2  3172  rexbii2  3176  rexcom4  3180  risset  3194  reximdv2  3199  rexbidv2  3224  rspe  3233  nfre1  3235  reximd2a  3241  r19.23t  3242  rexbida  3247  ralrexbidOLD  3252  r19.12  3254  r19.12OLD  3255  r19.41v  3275  r19.41  3276  rexcom  3283  reeanlem  3292  rexeqf  3325  reu5  3352  rmo5  3356  cbvrexvw  3374  cbvrexdva2  3383  rexv  3448  2gencl  3463  3gencl  3464  rspce  3541  ceqsrexv  3579  rexabOLD  3626  rexab2  3631  rexab2OLD  3632  rexrab2  3633  morex  3650  reu2  3656  reu6  3657  reu3  3658  2reuswap  3677  2reuswap2  3678  2reu5lem3  3688  2reu5  3689  2rmoswap  3692  ssrexf  3982  rexdifi  4077  rexun  4121  reuun2  4246  reuss2  4247  reupick  4250  reupick3  4251  euelss  4253  reximdva0  4283  n0rex  4286  n0el  4293  r19.2z  4423  r19.2zb  4424  rexsns  4602  exsnrex  4613  dfuni2  4838  eluni2  4840  elunirab  4852  iuncom4  4929  iunxiun  5022  axrep6  5210  axsepgfromrep  5214  intexrab  5257  opeliunxp  5644  xpiundi  5647  xpiundir  5648  ssrelrn  5791  dmuni  5811  rnmpt  5852  elrnmpt1  5855  dfima2  5959  dfima3  5960  elima2  5963  dfco2a  6138  imaco  6143  elsnxp  6182  dfpo2  6187  dffo4  6958  dffo5  6959  abrexco  7096  isomin  7185  zfrep6  7768  opabex3d  7778  opabex3rd  7779  opabex3  7780  abexssex  7783  abexex  7784  frxp  7935  dfrecs3  8151  rdglim2  8210  oarec  8332  oeeu  8373  mapsnd  8609  mapsnend  8757  pssnn  8890  pwfir  8898  enfii  8909  pssnnOLD  8943  unblem2  8972  dffi2  9087  marypha2lem4  9102  marypha2  9103  zfregcl  9258  axinf2  9303  zfinf2  9305  rankuni  9527  scott0  9550  cp  9555  bnd2  9557  infpwfien  9724  aceq1  9779  dfac5lem2  9786  dfac5lem3  9787  dfac2b  9792  kmlem3  9814  kmlem6  9817  kmlem8  9819  kmlem14  9825  infmap2  9880  ackbij2  9905  cfub  9911  cfval2  9922  cflim3  9924  cfss  9927  cfslb  9928  isf32lem9  10023  zorn2lem6  10163  iundom2g  10202  winalim2  10358  grothprim  10496  genpass  10671  nqpr  10676  1idpr  10691  ltexprlem4  10701  ltexprlem5  10702  reclem2pr  10710  axrrecex  10825  dedekind  11043  sup2  11836  infm3  11839  nnunb  12134  2rexuz  12544  nnwos  12559  xrsupsslem  12945  xrinfmsslem  12946  hashgt23el  14042  ishashinf  14080  cshwsexa  14440  wwlktovfo  14576  maxprmfct  16317  vdwapun  16578  vdwmc  16582  vdwmc2  16583  ram0  16626  imasleval  17144  mreexexlem2d  17246  dfiso2  17376  isssc  17424  drsdirfi  17913  dirge  18211  pwmnd  18466  psgnunilem4  18995  odcau  19099  ablfac2  19582  lspprat  20305  lidlnz  20387  isbasis2g  21981  tgval2  21989  ntreq0  22111  neitr  22214  cmpfi  22442  is1stc2  22476  2ndcsb  22483  2ndcsep  22493  1stcelcls  22495  hausmapdom  22534  isfbas2  22869  fbssint  22872  isfil2  22890  elfg  22905  fgcl  22912  uffix2  22958  alexsubALTlem4  23084  lpbl  23540  metustexhalf  23593  metuel2  23602  restmetu  23607  bcthlem5  24372  upgrex  27340  uvtx01vtx  27642  uhgrvd00  27779  wlkswwlksf1o  28120  wwlksnextsurj  28141  frcond3  28509  frgr3vlem2  28514  3vfriswmgrlem  28517  frgrncvvdeqlem9  28547  ubthlem1  29108  axhcompl-zf  29236  isch3  29479  shne0i  29686  cnlnssadj  30318  reuxfrdf  30715  rexunirn  30716  rmoxfrd  30717  dmrab  30720  abrexdomjm  30728  abrexexd  30730  iunrnmptss  30781  1stpreimas  30915  fpwrelmapffslem  30944  qsxpid  31435  krull  31520  zarclsint  31699  ordtconnlem1  31751  ddemeas  32079  omssubaddlem  32141  omssubadd  32142  eulerpartlemgvv  32218  tgoldbachgt  32518  bnj168  32584  bnj956  32631  bnj1098  32638  bnj1143  32645  bnj1146  32646  bnj1185  32648  bnj1196  32649  bnj600  32774  bnj849  32780  bnj906  32785  bnj916  32788  bnj983  32806  bnj984  32807  bnj1083  32833  bnj1176  32860  bnj1186  32862  bnj1189  32864  bnj1228  32866  bnj1253  32872  bnj1398  32889  bnj1463  32910  bnj1312  32913  bnj1514  32918  exdifsn  32928  lfuhgr3  32956  cusgredgex  32958  loop1cycl  32974  erdszelem10  33037  ptpconn  33070  imaeqsexv  33568  coep  33600  coepr  33601  dffr5  33602  opelco3  33630  dfon2lem8  33647  brttrcl2  33675  ttrclselem2  33687  lrrecfr  34002  brimg  34141  dfrecs2  34154  dfrdg4  34155  ellines  34356  neifg  34462  bj-rexvw  34967  bj-gabima  35030  bj-snglc  35061  bj-snglss  35062  bj-rest10  35162  bj-restn0  35164  bj-restpw  35166  bj-rest0  35167  bj-restb  35168  bj-restuni  35171  bj-dfmpoa  35192  bj-finsumval0  35359  rnmptsn  35412  f1omptsnlem  35413  mptsnunlem  35415  topdifinffinlem  35424  isbasisrelowllem1  35432  isbasisrelowllem2  35433  relowlpssretop  35441  fvineqsneq  35489  pibt2  35494  poimirlem30  35713  abrexdom  35794  prdstotbnd  35858  eldmqsres2  36328  exanres  36336  rncnvepres  36345  rnxrnres  36431  1cossres  36458  eldm1cossres  36484  eldmqs1cossres  36677  prtlem17  36796  prter2  36801  islshpat  36937  lsat0cv  36953  lshpsmreu  37029  atex  37326  islpln5  37455  islvol5  37499  pmapglb  37690  pmapglb2N  37691  pmapglb2xN  37692  elpaddn0  37720  pmapjat1  37773  polval2N  37826  osumcllem11N  37886  pexmidlem8N  37897  cdlemftr3  38485  dibelval3  39067  dibglbN  39086  dicelval3  39100  dihglbcpreN  39220  dihglb2  39262  dihjatcclem4  39341  mapdordlem2  39557  mapdrvallem2  39565  mapdpglem3  39595  hdmapglem7a  39847  sticksstones3  40004  imaopab  40105  sn-sup2  40332  prjspeclsp  40344  rp-isfinite5  40994  rp-isfinite6  40995  elintima  41123  iunrelexpuztr  41189  cotrclrcl  41212  neik0pk1imk0  41519  ntrneineine0lem  41555  ntrneineine1lem  41556  ntrneiel2  41558  cpcolld  41738  expandrexn  41771  ismnuprim  41774  rr-grothprimbi  41775  rr-groth  41779  ismnushort  41781  rr-grothshortbi  41783  rexbidar  41926  onfrALTlem5  42024  onfrALTlem2  42028  onfrALTlem1  42030  onfrALTlem5VD  42367  onfrALTlem2VD  42371  onfrALTlem1VD  42372  chordthmALT  42415  rspcegf  42428  cncmpmax  42437  rfcnnnub  42441  inn0f  42483  nssrex  42498  eluni2f  42515  eliin2f  42516  suprnmpt  42572  founiiun0  42590  disjinfi  42593  fvelima2  42668  ssfiunibd  42711  infrpge  42753  fsumiunss  42979  islpcn  43043  lptre2pt  43044  stoweidlem14  43418  stoweidlem34  43438  stoweidlem35  43439  stoweidlem43  43447  stoweidlem44  43448  stoweidlem50  43454  stoweidlem54  43458  stoweidlem56  43460  stoweidlem59  43463  stoweidlem60  43464  fourier2  43631  qndenserrnbllem  43698  qndenserrn  43703  sge0rpcpnf  43822  hoidmvval0b  43991  hoiqssbllem3  44025  imasetpreimafvbijlemfv1  44716  nfermltl8rev  45055  nfermltl2rev  45056  nfermltlrev  45057  nn0mnd  45234  opeliun2xp  45529  rextru  46010  opncldeqv  46056  opnneilv  46063  setrec1lem3  46254