MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rex Structured version   Visualization version   GIF version

Definition df-rex 2902
Description: Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22. (Contributed by NM, 30-Aug-1993.)
Assertion
Ref Expression
df-rex (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))

Detailed syntax breakdown of Definition df-rex
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
3 cA . . 3 class 𝐴
41, 2, 3wrex 2897 . 2 wff 𝑥𝐴 𝜑
52cv 1474 . . . . 5 class 𝑥
65, 3wcel 1977 . . . 4 wff 𝑥𝐴
76, 1wa 383 . . 3 wff (𝑥𝐴𝜑)
87, 2wex 1695 . 2 wff 𝑥(𝑥𝐴𝜑)
94, 8wb 195 1 wff (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  ralnex  2975  ralnexOLD  2976  rexex  2985  rspe  2986  nfre1  2988  reximi2  2993  reximd2a  2996  reximdv2  2997  r19.23t  3003  rexbii2  3021  rexbida  3029  rexbidv2  3030  risset  3044  r19.41v  3070  r19.41  3071  reean  3085  rexeqf  3112  reu5  3136  rmo5  3139  cbvrexdva2  3152  rexv  3193  2gencl  3209  3gencl  3210  rspce  3277  ceqsrexv  3306  rexab  3336  rexab2  3340  rexrab2  3341  morex  3357  reu2  3361  reu6  3362  reu3  3363  2reuswap  3377  2reu5lem3  3382  2reu5  3383  ssrexf  3628  rexun  3755  reuss2  3866  reuun2  3869  reupick  3870  reupick3  3871  euelss  3873  reximdva0  3891  rabn0OLD  3913  r19.2z  4012  r19.2zb  4013  rexsns  4164  exsnrex  4168  dfuni2  4374  eluni2  4376  elunirab  4384  iuncom4  4464  iunxiun  4544  intexrab  4750  elxp2OLD  5057  opeliunxp  5093  xpiundi  5096  xpiundir  5097  ssrelrn  5237  dmuni  5256  rnmpt  5292  elrnmpt1  5295  elres  5355  dfima2  5387  dfima3  5388  elima2  5391  dfco2a  5552  imaco  5557  elsnxp  5594  elsnxpOLD  5595  dffo4  6283  dffo5  6284  abrexco  6406  isomin  6487  zfrep6  7027  opabex3d  7037  opabex3  7038  abexssex  7041  abexex  7042  frxp  7174  dfrecs3  7356  rdglim2  7415  oarec  7529  oeeu  7570  mapsn  7785  mapsnen  7920  pssnn  8063  unblem2  8098  dffi2  8212  marypha2lem4  8227  marypha2  8228  zfregcl  8382  zfregclOLD  8384  axinf2  8420  zfinf2  8422  rankuni  8609  scott0  8632  cp  8637  bnd2  8639  infpwfien  8768  aceq1  8823  dfac5lem2  8830  dfac5lem3  8831  dfac2  8836  kmlem3  8857  kmlem6  8860  kmlem8  8862  kmlem14  8868  infmap2  8923  ackbij2  8948  cfub  8954  cfval2  8965  cflim3  8967  cfss  8970  cfslb  8971  isf32lem9  9066  zorn2lem6  9206  iundom2g  9241  winalim2  9397  grothprim  9535  genpass  9710  nqpr  9715  1idpr  9730  ltexprlem4  9740  ltexprlem5  9741  reclem2pr  9749  axrrecex  9863  dedekind  10079  sup2  10858  infm3  10861  nnunb  11165  2rexuz  11616  nnwos  11631  xrsupsslem  12009  xrinfmsslem  12010  ishashinf  13104  cshwsexa  13421  wwlktovfo  13549  ncoprmgcdne1b  15201  maxprmfct  15259  vdwapun  15516  vdwmc  15520  vdwmc2  15521  ram0  15564  imasleval  16024  mreexexlem2d  16128  dfiso2  16255  isssc  16303  drsdirfi  16761  dirge  17060  psgnunilem4  17740  odcau  17842  ablfac2  18311  lspprat  18974  lidlnz  19049  isbasis2g  20563  tgval2  20571  ntreq0  20691  neitr  20794  cmpfi  21021  is1stc2  21055  2ndcsb  21062  2ndcsep  21072  1stcelcls  21074  hausmapdom  21113  isfbas2  21449  fbssint  21452  isfil2  21470  elfg  21485  fgcl  21492  uffix2  21538  alexsubALTlem4  21664  lpbl  22118  metustexhalf  22171  metuel2  22180  restmetu  22185  bcthlem5  22933  upgrex  25759  umgraex  25852  usgraedg4  25916  uvtx01vtx  26020  3v3e3cycl2  26192  wlknwwlknsur  26240  wlkiswwlksur  26247  wwlkextsur  26259  frisusgranb  26524  frgra3vlem2  26528  3vfriswmgralem  26531  frgrancvvdeqlemC  26566  usg2spot2nb  26592  ubthlem1  27110  axhcompl-zf  27239  isch3  27482  shne0i  27691  cnlnssadj  28323  2reuswap2  28712  rexunirn  28715  rmoxfrdOLD  28716  rmoxfrd  28717  abrexdomjm  28729  abrexexd  28731  iunxsngf  28758  1stpreimas  28866  fpwrelmapffslem  28895  ordtconlem1  29298  ddemeas  29626  omssubaddlem  29688  omssubadd  29689  eulerpartlemgvv  29765  bnj168  30052  bnj956  30101  bnj1098  30108  bnj1143  30115  bnj1146  30116  bnj1185  30118  bnj1196  30119  bnj600  30243  bnj849  30249  bnj906  30254  bnj916  30257  bnj983  30275  bnj984  30276  bnj1083  30300  bnj1176  30327  bnj1186  30329  bnj1189  30331  bnj1228  30333  bnj1253  30339  bnj1398  30356  bnj1463  30377  bnj1312  30380  bnj1514  30385  erdszelem10  30436  ptpcon  30469  coep  30894  coepr  30895  dffr5  30896  dfpo2  30898  opelco3  30923  dfon2lem8  30939  brimg  31214  dfrecs2  31227  dfrdg4  31228  ellines  31429  neifg  31536  bj-rexvwv  32060  bj-rexcom4  32063  bj-snglc  32150  bj-snglss  32151  bj-rest10  32222  bj-restn0  32224  bj-restpw  32226  bj-rest0  32227  bj-restb  32228  bj-restuni  32231  bj-dfmpt2a  32252  bj-finsumval0  32324  rnmptsn  32358  f1omptsnlem  32359  mptsnunlem  32361  topdifinffinlem  32371  isbasisrelowllem1  32379  isbasisrelowllem2  32380  relowlpssretop  32388  poimirlem30  32609  abrexdom  32695  prdstotbnd  32763  n0el  33164  prtlem17  33179  prter2  33184  islshpat  33322  lsat0cv  33338  lshpsmreu  33414  atex  33710  islpln5  33839  islvol5  33883  pmapglb  34074  pmapglb2N  34075  pmapglb2xN  34076  elpaddn0  34104  pmapjat1  34157  polval2N  34210  osumcllem11N  34270  pexmidlem8N  34281  cdlemftr3  34871  dibelval3  35454  dibglbN  35473  dicelval3  35487  dihglbcpreN  35607  dihglb2  35649  dihjatcclem4  35728  mapdordlem2  35944  mapdrvallem2  35952  mapdpglem3  35982  hdmapglem7a  36237  rp-isfinite5  36882  rp-isfinite6  36883  relintabex  36906  elintima  36964  iunrelexpuztr  37030  cotrclrcl  37053  neik0pk1imk0  37365  ntrneineine0lem  37401  ntrneineine1lem  37402  ntrneiel2  37404  rexbidar  37671  onfrALTlem5  37778  onfrALTlem2  37782  onfrALTlem1  37784  onfrALTlem5VD  38143  onfrALTlem2VD  38147  onfrALTlem1VD  38148  chordthmALT  38191  rspcegf  38205  cncmpmax  38214  rfcnnnub  38218  rspcef  38267  inn0f  38268  nssrex  38287  eluni2f  38315  eliin2f  38316  suprnmpt  38350  founiiun0  38372  disjinfi  38375  mapsnd  38383  mapsnend  38386  ssfiunibd  38464  infrpge  38508  fsumiunss  38642  islpcn  38706  lptre2pt  38707  stoweidlem14  38907  stoweidlem34  38927  stoweidlem35  38928  stoweidlem43  38936  stoweidlem44  38937  stoweidlem50  38943  stoweidlem54  38947  stoweidlem56  38949  stoweidlem59  38952  stoweidlem60  38953  fourier2  39120  qndenserrnbllem  39190  qndenserrn  39195  sge0rpcpnf  39314  hoidmvval0b  39480  hoiqssbllem3  39514  2rmoswap  39833  n0rex  40310  uvtxa01vtx0  40623  uhgrvd00  40750  1wlkpwwlkf1ouspgr  41076  wlknwwlksnsur  41087  wlkwwlksur  41094  wwlksnextsur  41106  frcond3  41440  frgr3vlem2  41444  3vfriswmgrlem  41447  frgrncvvdeqlemC  41478  fusgr2wsp2nb  41498  opeliun2xp  41904  setrec1lem3  42235
  Copyright terms: Public domain W3C validator