Definition df-rex 3091

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 3081). (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 3090	. 2 wff ∃𝑥 ∈ 𝐴 𝜑
5	2	cv 1569	. . . . 5 class 𝑥
6	5, 3	wcel 2147	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 401	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	wex 1812	. 2 wff ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)
9	4, 8	wb 209	1 wff (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is used by:  ralnex  3092  rexex  3096  rextru  3097  reximi2  3099  rexbii2  3109  rexlimiva  3159  reximdv2  3176  rexbidv2  3186  r19.41v  3196  r3ex  3205  reeanlem  3237  risset  3241  cbvrexvw  3245  rspe  3256  r19.23t  3262  r19.41  3270  reximd2a  3276  rexbida  3278  nfre1  3291  rexcom4  3293  r19.12  3315  rexeq  3319  reu5  3371  rmo5  3387  rexv  3481  2gencl  3496  3gencl  3497  rspce  3569  ceqsrexv  3612  rexab2  3660  rexrab2  3661  morex  3680  reu2  3686  reu6  3687  reu3  3688  2reuswap  3707  2reuswap2  3708  2reu5lem3  3718  2reu5  3719  2rmoswap  3722  nssrex  3978  ssrexf  3980  ssrexv  3983  rexss  3987  rexdifi  4089  rexun  4197  reuun2  4273  reuss2  4274  reupick  4277  reupick3  4278  euelss  4280  reximdva0  4306  n0rex  4308  n0el  4315  inn0f  4322  r19.2z  4458  rexsns  4632  exsnrex  4641  dfuni2  4872  eluni2  4874  elunirab  4885  iuncom4  4963  iunxiun  5060  axrep6  5243  replem  5244  axsepgfromrep  5250  intexrab  5312  opeliunxp  5722  opeliun2xp  5723  xpiundi  5726  xpiundir  5727  ssrelrn  5882  dmuni  5902  rnmpt  5945  elrnmpt1  5948  dfima2  6069  dfima3  6070  elima2  6073  dfco2a  6259  imaco  6264  elsnxp  6309  dfpo2  6314  fvelima2  6957  dffo4  7124  dffo5  7125  abrexco  7268  isomin  7365  imaeqexov  7680  zfrep6OLD  7988  opabex3d  7998  opabex3rd  7999  opabex3  8000  abexssex  8003  abexex  8004  frxp  8162  dfrecs3  8405  rdglim2  8465  oarec  8595  oeeu  8637  mapsnd  8939  mapsnend  9089  pssnn  9209  enfii  9226  enp1i  9295  unblem2  9310  pwfir  9333  dffi2  9439  marypha2lem4  9454  marypha2  9455  zfregcl  9612  zfregclOLD  9613  axinf2  9665  zfinf2  9667  brttrcl2  9739  ttrclselem2  9751  rankuni  9903  r1filimi  9927  scott0b  9961  scott0OLD  9962  cp  9978  bnd2  9980  setrec1lem3  9993  infpwfien  10165  aceq1  10220  dfac5lem2  10227  dfac5lem3  10228  dfac2b  10233  kmlem3  10255  kmlem6  10258  kmlem8  10260  kmlem14  10266  infmap2  10319  ackbij2  10344  cfub  10350  cfval2  10362  cflim3  10364  cfss  10367  cfslb  10368  isf32lem9  10463  zorn2lem6  10603  iundom2g  10648  winalim2  10805  grothprim  10943  genpass  11118  nqpr  11123  1idpr  11138  ltexprlem4  11148  ltexprlem5  11149  reclem2pr  11157  axrrecex  11272  dedekind  11497  sup2  12297  infm3  12300  nnunb  12626  2rexuz  13051  nnwos  13066  xrsupsslem  13461  xrinfmsslem  13462  hashgt23el  14593  ishashinf  14632  wwlktovfo  15137  maxprmfct  16911  vdwapun  17178  vdwmc  17182  vdwmc2  17183  ram0  17226  imasleval  17739  mreexexlem2d  17845  dfiso2  17973  isssc  18021  drsdirfi  18505  dirge  18803  pwmnd  19169  qsxpid  19413  psgnunilem4  19738  odcau  19845  ablfac2  20332  lspprat  21458  lidlnz  21557  isbasis2g  23293  tgval2  23301  ntreq0  23422  neitr  23525  cmpfi  23753  is1stc2  23787  2ndcsb  23794  2ndcsep  23805  1stcelcls  23807  hausmapdom  23846  isfbas2  24181  fbssint  24184  isfil2  24202  elfg  24217  fgcl  24224  uffix2  24270  alexsubALTlem4  24396  lpbl  24849  metustexhalf  24902  metuel2  24911  restmetu  24916  bcthlem5  25676  lrrecfr  28356  upgrex  29697  lfuhgr3  29755  uvtx01vtx  30005  uhgrvd00  30142  wlkswwlksf1o  30495  wwlksnextsurj  30516  loop1cycl  30771  frcond3  30897  frgr3vlem2  30902  3vfriswmgrlem  30905  frgrncvvdeqlem9  30935  ubthlem1  31499  axhcompl-zf  31627  isch3  31870  shne0i  32077  cnlnssadj  32709  reuxfrdf  33156  rexunirn  33157  rmoxfrd  33158  dmrab  33162  abrexdomjm  33172  abrexexd  33174  iunrnmptss  33228  ac6mapd  33286  1stpreimas  33367  fpwrelmapffslem  33391  krull  34070  zarclsint  34571  ordtconnlem1  34623  ddemeas  34936  omssubaddlem  34998  omssubadd  34999  eulerpartlemgvv  35075  tgoldbachgt  35359  bnj168  35428  bnj956  35474  bnj1098  35481  bnj1143  35487  bnj1146  35488  bnj1185  35490  bnj1196  35491  bnj600  35616  bnj849  35622  bnj906  35627  bnj916  35630  bnj983  35648  bnj984  35649  bnj1083  35675  bnj1176  35702  bnj1186  35704  bnj1189  35706  bnj1228  35708  bnj1253  35714  bnj1398  35731  bnj1463  35752  bnj1312  35755  bnj1514  35760  reu6f  35776  rmo6  35777  exdifsn  35780  axprALT2  35815  axregszf  35896  karddom  35928  kardsdom  35929  kardfi  35937  onvf1odlem1  36030  onvf1odlem2  36031  wevgblacfn  36038  cusgredgex  36062  erdszelem10  36131  ptpconn  36164  rexxfr3dALT  36570  mirimanofffr  36628  coep  36694  coepr  36695  dffr5  36696  opelco3  36716  dfon2lem8  36729  brimg  36876  dfrecs2  36891  dfrdg4  36892  ellines  37094  cbvrexvw2  37193  neifg  37336  regsfromunir1  37505  bj-rexvw  37969  bj-gabima  38030  bj-snglc  38059  bj-snglss  38060  bj-dfres2  38140  bj-axseprep  38180  bj-axreprepsep  38181  bj-rest10  38199  bj-restn0  38201  bj-restpw  38203  bj-rest0  38204  bj-restb  38205  bj-restuni  38208  bj-dfmpoa  38230  bj-finsumval0  38397  rnmptsn  38449  f1omptsnlem  38450  mptsnunlem  38452  topdifinffinlem  38461  isbasisrelowllem1  38469  isbasisrelowllem2  38470  relowlpssretop  38478  fvineqsneq  38526  pibt2  38531  poimirlem30  38759  negprop  38834  impprop  38835  dfprop1  38836  abrexdom  38855  prdstotbnd  38919  elrnres  39401  eldmqsres2  39417  exanres  39424  rncnvepres  39432  rnxrnres  39545  1cossres  39642  eldm1cossres  39673  eldmqs1cossres  39867  disjlem17  40025  disjdmqscossss  40029  prtlem17  40124  prter2  40129  islshpat  40265  lsat0cv  40281  lshpsmreu  40357  atex  40654  islpln5  40783  islvol5  40827  pmapglb  41018  pmapglb2N  41019  pmapglb2xN  41020  elpaddn0  41048  pmapjat1  41101  polval2N  41154  osumcllem11N  41214  pexmidlem8N  41225  cdlemftr3  41813  dibelval3  42395  dibglbN  42414  dicelval3  42428  dihglbcpreN  42548  dihglb2  42590  dihjatcclem4  42669  mapdrvallem2  42893  mapdpglem3  42923  hdmapglem7a  43175  sticksstones3  43389  imaopab  43476  sn-sup2  43746  fimgmcyc  43789  prjspeclsp  43831  uniel  44409  nnoeomeqom  44504  tfsconcatlem  44528  tfsconcatrn  44534  tfsconcat0i  44537  rp-isfinite5  44708  rp-isfinite6  44709  minregex  44725  elintima  44843  iunrelexpuztr  44909  cotrclrcl  44932  neik0pk1imk0  45237  ntrneineine0lem  45273  ntrneineine1lem  45274  ntrneiel2  45276  cpcolld  45432  expandrexn  45465  ismnuprim  45468  rr-grothprimbi  45469  rr-groth  45473  ismnushort  45475  rr-grothshortbi  45477  rexbidar  45618  onfrALTlem5  45714  onfrALTlem2  45718  onfrALTlem1  45720  onfrALTlem5VD  46056  onfrALTlem2VD  46060  onfrALTlem1VD  46061  chordthmALT  46104  rspesbcd  46109  modelaxreplem3  46163  ssclaxsep  46165  permaxrep  46189  nregmodel  46200  rspcegf  46243  cncmpmax  46252  rfcnnnub  46256  eluni2f  46321  eliin2f  46322  suprnmpt  46392  founiiun0  46408  disjinfi  46410  ssfiunibd  46528  infrpge  46566  fsumiunss  46790  islpcn  46852  lptre2pt  46853  stoweidlem14  47227  stoweidlem34  47247  stoweidlem35  47248  stoweidlem43  47256  stoweidlem44  47257  stoweidlem50  47263  stoweidlem54  47267  stoweidlem56  47269  stoweidlem59  47272  stoweidlem60  47273  fourier2  47440  qndenserrnbllem  47507  qndenserrn  47512  sge0rpcpnf  47634  hoidmvval0b  47803  hoiqssbllem3  47837  tmachlem-exagreecover  48159  imasetpreimafvbijlemfv1  48688  nfermltl8rev  49043  nfermltl2rev  49044  nfermltlrev  49045  isubgredg  49167  gpg5edgnedg  49431  nn0mnd  49479  opncldbid  50219  opnneilv  50226  dfrals2  51164