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

This definition is referenced by:  ralnex  3073  rexex  3077  rextru  3078  reximi2  3080  rexbii2  3091  ralrexbidOLD  3108  rexlimiva  3148  reximdv2  3165  rexbidv2  3175  r19.41v  3189  reeanlem  3226  risset  3231  cbvrexvw  3236  rspe  3247  r19.23t  3253  r19.41  3261  reximd2a  3267  rexbida  3270  nfre1  3283  rexcom4  3286  rexcomOLD  3289  r19.12  3312  r19.12OLD  3313  rexeq  3322  cbvrexdva2OLD  3347  rexeqfOLD  3352  reu5  3379  rmo5  3397  rexv  3500  2gencl  3516  3gencl  3517  rspce  3601  ceqsrexv  3642  rexabOLD  3690  rexab2  3694  rexrab2  3695  morex  3714  reu2  3720  reu6  3721  reu3  3722  2reuswap  3741  2reuswap2  3742  2reu5lem3  3752  2reu5  3753  2rmoswap  3756  ssrexf  4047  rexdifi  4144  rexun  4189  reuun2  4313  reuss2  4314  reupick  4317  reupick3  4318  euelss  4320  reximdva0  4350  n0rex  4353  n0el  4360  r19.2z  4493  r19.2zb  4494  rexsns  4672  exsnrex  4683  dfuni2  4909  eluni2  4911  elunirab  4923  iuncom4  5004  iunxiun  5099  axrep6  5291  axsepgfromrep  5296  intexrab  5339  opeliunxp  5741  xpiundi  5744  xpiundir  5745  ssrelrn  5892  dmuni  5912  rnmpt  5952  elrnmpt1  5955  dfima2  6059  dfima3  6060  elima2  6063  dfco2a  6242  imaco  6247  elsnxp  6287  dfpo2  6292  dffo4  7100  dffo5  7101  abrexco  7238  isomin  7329  imaeqsexv  7355  imaeqexov  7640  zfrep6  7936  opabex3d  7947  opabex3rd  7948  opabex3  7949  abexssex  7952  abexex  7953  frxp  8107  dfrecs3  8367  dfrecs3OLD  8368  rdglim2  8427  oarec  8558  oeeu  8599  mapsnd  8876  mapsnend  9032  pssnn  9164  pwfir  9172  enfii  9185  pssnnOLD  9261  enp1i  9275  unblem2  9292  dffi2  9414  marypha2lem4  9429  marypha2  9430  zfregcl  9585  axinf2  9631  zfinf2  9633  brttrcl2  9705  ttrclselem2  9717  rankuni  9854  scott0  9877  cp  9882  bnd2  9884  infpwfien  10053  aceq1  10108  dfac5lem2  10115  dfac5lem3  10116  dfac2b  10121  kmlem3  10143  kmlem6  10146  kmlem8  10148  kmlem14  10154  infmap2  10209  ackbij2  10234  cfub  10240  cfval2  10251  cflim3  10253  cfss  10256  cfslb  10257  isf32lem9  10352  zorn2lem6  10492  iundom2g  10531  winalim2  10687  grothprim  10825  genpass  11000  nqpr  11005  1idpr  11020  ltexprlem4  11030  ltexprlem5  11031  reclem2pr  11039  axrrecex  11154  dedekind  11373  sup2  12166  infm3  12169  nnunb  12464  2rexuz  12880  nnwos  12895  xrsupsslem  13282  xrinfmsslem  13283  hashgt23el  14380  ishashinf  14420  cshwsexaOLD  14771  wwlktovfo  14905  maxprmfct  16642  vdwapun  16903  vdwmc  16907  vdwmc2  16908  ram0  16951  imasleval  17483  mreexexlem2d  17585  dfiso2  17715  isssc  17763  drsdirfi  18254  dirge  18552  pwmnd  18814  psgnunilem4  19358  odcau  19465  ablfac2  19951  lspprat  20754  lidlnz  20840  isbasis2g  22433  tgval2  22441  ntreq0  22563  neitr  22666  cmpfi  22894  is1stc2  22928  2ndcsb  22935  2ndcsep  22945  1stcelcls  22947  hausmapdom  22986  isfbas2  23321  fbssint  23324  isfil2  23342  elfg  23357  fgcl  23364  uffix2  23410  alexsubALTlem4  23536  lpbl  23994  metustexhalf  24047  metuel2  24056  restmetu  24061  bcthlem5  24827  lrrecfr  27407  upgrex  28332  uvtx01vtx  28634  uhgrvd00  28771  wlkswwlksf1o  29113  wwlksnextsurj  29134  frcond3  29502  frgr3vlem2  29507  3vfriswmgrlem  29510  frgrncvvdeqlem9  29540  ubthlem1  30101  axhcompl-zf  30229  isch3  30472  shne0i  30679  cnlnssadj  31311  reuxfrdf  31709  rexunirn  31710  rmoxfrd  31711  dmrab  31715  abrexdomjm  31722  abrexexd  31724  iunrnmptss  31775  1stpreimas  31905  fpwrelmapffslem  31935  qsxpid  32443  krull  32547  zarclsint  32790  ordtconnlem1  32842  ddemeas  33172  omssubaddlem  33236  omssubadd  33237  eulerpartlemgvv  33313  tgoldbachgt  33613  bnj168  33679  bnj956  33725  bnj1098  33732  bnj1143  33739  bnj1146  33740  bnj1185  33742  bnj1196  33743  bnj600  33868  bnj849  33874  bnj906  33879  bnj916  33882  bnj983  33900  bnj984  33901  bnj1083  33927  bnj1176  33954  bnj1186  33956  bnj1189  33958  bnj1228  33960  bnj1253  33966  bnj1398  33983  bnj1463  34004  bnj1312  34007  bnj1514  34012  exdifsn  34022  lfuhgr3  34048  cusgredgex  34050  loop1cycl  34066  erdszelem10  34129  ptpconn  34162  coep  34660  coepr  34661  dffr5  34662  opelco3  34684  dfon2lem8  34700  brimg  34847  dfrecs2  34860  dfrdg4  34861  ellines  35062  neifg  35194  bj-rexvw  35698  bj-gabima  35758  bj-snglc  35788  bj-snglss  35789  bj-rest10  35907  bj-restn0  35909  bj-restpw  35911  bj-rest0  35912  bj-restb  35913  bj-restuni  35916  bj-dfmpoa  35937  bj-finsumval0  36104  rnmptsn  36154  f1omptsnlem  36155  mptsnunlem  36157  topdifinffinlem  36166  isbasisrelowllem1  36174  isbasisrelowllem2  36175  relowlpssretop  36183  fvineqsneq  36231  pibt2  36236  poimirlem30  36456  abrexdom  36536  prdstotbnd  36600  elrnres  37077  eldmqsres2  37094  exanres  37102  rncnvepres  37110  rnxrnres  37207  1cossres  37237  eldm1cossres  37268  eldmqs1cossres  37467  disjlem17  37607  disjdmqscossss  37611  prtlem17  37684  prter2  37689  islshpat  37825  lsat0cv  37841  lshpsmreu  37917  atex  38215  islpln5  38344  islvol5  38388  pmapglb  38579  pmapglb2N  38580  pmapglb2xN  38581  elpaddn0  38609  pmapjat1  38662  polval2N  38715  osumcllem11N  38775  pexmidlem8N  38786  cdlemftr3  39374  dibelval3  39956  dibglbN  39975  dicelval3  39989  dihglbcpreN  40109  dihglb2  40151  dihjatcclem4  40230  mapdordlem2  40446  mapdrvallem2  40454  mapdpglem3  40484  hdmapglem7a  40736  sticksstones3  40902  imaopab  40999  sn-sup2  41286  prjspeclsp  41298  uniel  41899  nnoeomeqom  41995  tfsconcatlem  42019  tfsconcatrn  42025  tfsconcat0i  42028  rp-isfinite5  42201  rp-isfinite6  42202  minregex  42218  elintima  42337  iunrelexpuztr  42403  cotrclrcl  42426  neik0pk1imk0  42731  ntrneineine0lem  42767  ntrneineine1lem  42768  ntrneiel2  42770  cpcolld  42950  expandrexn  42983  ismnuprim  42986  rr-grothprimbi  42987  rr-groth  42991  ismnushort  42993  rr-grothshortbi  42995  rexbidar  43138  onfrALTlem5  43236  onfrALTlem2  43240  onfrALTlem1  43242  onfrALTlem5VD  43579  onfrALTlem2VD  43583  onfrALTlem1VD  43584  chordthmALT  43627  rspcegf  43640  cncmpmax  43649  rfcnnnub  43653  inn0f  43693  nssrex  43708  eluni2f  43725  eliin2f  43726  suprnmpt  43803  founiiun0  43821  disjinfi  43824  fvelima2  43899  ssfiunibd  43954  infrpge  43996  fsumiunss  44226  islpcn  44290  lptre2pt  44291  stoweidlem14  44665  stoweidlem34  44685  stoweidlem35  44686  stoweidlem43  44694  stoweidlem44  44695  stoweidlem50  44701  stoweidlem54  44705  stoweidlem56  44707  stoweidlem59  44710  stoweidlem60  44711  fourier2  44878  qndenserrnbllem  44945  qndenserrn  44950  sge0rpcpnf  45072  hoidmvval0b  45241  hoiqssbllem3  45275  imasetpreimafvbijlemfv1  46006  nfermltl8rev  46345  nfermltl2rev  46346  nfermltlrev  46347  nn0mnd  46524  opeliun2xp  46910  opncldeqv  47436  opnneilv  47443  setrec1lem3  47636