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 3102
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 3097 . 2 wff 𝑥𝐴 𝜑
52cv 1636 . . . . 5 class 𝑥
65, 3wcel 2156 . . . 4 wff 𝑥𝐴
76, 1wa 384 . . 3 wff (𝑥𝐴𝜑)
87, 2wex 1859 . 2 wff 𝑥(𝑥𝐴𝜑)
94, 8wb 197 1 wff (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  rexanid  3107  ralnex  3180  rexex  3189  rspe  3190  nfre1  3192  reximi2  3197  reximd2a  3200  reximdv2  3201  r19.23t  3209  rexbii2  3227  rexbida  3235  rexbidv2  3236  risset  3250  r19.41v  3277  r19.41  3278  reean  3294  rexeqf  3324  reu5  3348  rmo5  3351  cbvrexdva2  3365  rexv  3414  2gencl  3430  3gencl  3431  rspce  3497  ceqsrexv  3530  rexab  3565  rexab2  3569  rexrab2  3570  morex  3588  reu2  3592  reu6  3593  reu3  3594  2reuswap  3608  2reu5lem3  3613  2reu5  3614  ssrexf  3862  rexun  3992  reuss2  4108  reuun2  4111  reupick  4112  reupick3  4113  euelss  4115  reximdva0  4134  n0rex  4136  n0el  4141  r19.2z  4255  r19.2zb  4256  rexsns  4410  exsnrex  4414  dfuni2  4632  eluni2  4634  elunirab  4642  iuncom4  4720  iunxiun  4800  intexrab  5015  opeliunxp  5370  xpiundi  5373  xpiundir  5374  ssrelrn  5516  dmuni  5535  rnmpt  5572  elrnmpt1  5575  elresOLD  5639  dfima2  5678  dfima3  5679  elima2  5682  dfco2a  5849  imaco  5854  elsnxp  5891  dffo4  6593  dffo5  6594  abrexco  6722  isomin  6807  zfrep6  7360  opabex3d  7371  opabex3  7372  abexssex  7375  abexex  7377  frxp  7517  dfrecs3  7701  rdglim2  7760  oarec  7875  oeeu  7916  mapsnd  8130  mapsnend  8267  pssnn  8413  unblem2  8448  dffi2  8564  marypha2lem4  8579  marypha2  8580  zfregcl  8734  axinf2  8780  zfinf2  8782  rankuni  8969  scott0  8992  cp  8997  bnd2  8999  infpwfien  9164  aceq1  9219  dfac5lem2  9226  dfac5lem3  9227  dfac2b  9232  dfac2OLD  9234  kmlem3  9255  kmlem6  9258  kmlem8  9260  kmlem14  9266  infmap2  9321  ackbij2  9346  cfub  9352  cfval2  9363  cflim3  9365  cfss  9368  cfslb  9369  isf32lem9  9464  zorn2lem6  9604  iundom2g  9643  winalim2  9799  grothprim  9937  genpass  10112  nqpr  10117  1idpr  10132  ltexprlem4  10142  ltexprlem5  10143  reclem2pr  10151  axrrecex  10265  dedekind  10481  sup2  11260  infm3  11263  nnunb  11551  2rexuz  11954  nnwos  11970  xrsupsslem  12351  xrinfmsslem  12352  ishashinf  13460  cshwsexa  13790  wwlktovfo  13922  ncoprmgcdne1b  15578  maxprmfct  15634  vdwapun  15891  vdwmc  15895  vdwmc2  15896  ram0  15939  imasleval  16402  mreexexlem2d  16506  dfiso2  16632  isssc  16680  drsdirfi  17139  dirge  17438  psgnunilem4  18114  odcau  18216  ablfac2  18686  lspprat  19358  lidlnz  19433  isbasis2g  20962  tgval2  20970  ntreq0  21091  neitr  21194  cmpfi  21421  is1stc2  21455  2ndcsb  21462  2ndcsep  21472  1stcelcls  21474  hausmapdom  21513  isfbas2  21848  fbssint  21851  isfil2  21869  elfg  21884  fgcl  21891  uffix2  21937  alexsubALTlem4  22063  lpbl  22517  metustexhalf  22570  metuel2  22579  restmetu  22584  bcthlem5  23333  upgrex  26197  uvtx01vtx  26514  uvtxa01vtx0OLD  26516  uhgrvd00  26654  wlkswwlksf1o  27002  wlknwwlksnsurOLD  27013  wlkwwlksurOLD  27021  wwlksnextsur  27033  frcond3  27440  frgr3vlem2  27445  3vfriswmgrlem  27448  frgrncvvdeqlem9  27478  ubthlem1  28050  axhcompl-zf  28179  isch3  28422  shne0i  28631  cnlnssadj  29263  2reuswap2  29650  rexunirn  29653  rmoxfrdOLD  29654  rmoxfrd  29655  abrexdomjm  29666  abrexexd  29668  1stpreimas  29806  fpwrelmapffslem  29830  ordtconnlem1  30291  ddemeas  30620  omssubaddlem  30682  omssubadd  30683  eulerpartlemgvv  30759  tgoldbachgt  31062  bnj168  31117  bnj956  31165  bnj1098  31172  bnj1143  31179  bnj1146  31180  bnj1185  31182  bnj1196  31183  bnj600  31307  bnj849  31313  bnj906  31318  bnj916  31321  bnj983  31339  bnj984  31340  bnj1083  31364  bnj1176  31391  bnj1186  31393  bnj1189  31395  bnj1228  31397  bnj1253  31403  bnj1398  31420  bnj1463  31441  bnj1312  31444  bnj1514  31449  erdszelem10  31500  ptpconn  31533  coep  31958  coepr  31959  dffr5  31960  dfpo2  31962  opelco3  31993  dfon2lem8  32010  brimg  32360  dfrecs2  32373  dfrdg4  32374  ellines  32575  neifg  32682  bj-rexvwv  33169  bj-rexcom4  33172  bj-snglc  33262  bj-snglss  33263  bj-rest10  33347  bj-restn0  33349  bj-restpw  33351  bj-rest0  33352  bj-restb  33353  bj-restuni  33356  bj-dfmpt2a  33377  bj-finsumval0  33459  rnmptsn  33494  f1omptsnlem  33495  mptsnunlem  33497  topdifinffinlem  33506  isbasisrelowllem1  33514  isbasisrelowllem2  33515  relowlpssretop  33523  poimirlem30  33747  abrexdom  33832  prdstotbnd  33899  eldmqsres2  34364  exanres  34375  rncnvepres  34384  rnxrnres  34465  1cossres  34492  eldm1cossres  34518  prtlem17  34650  prter2  34655  islshpat  34792  lsat0cv  34808  lshpsmreu  34884  atex  35181  islpln5  35310  islvol5  35354  pmapglb  35545  pmapglb2N  35546  pmapglb2xN  35547  elpaddn0  35575  pmapjat1  35628  polval2N  35681  osumcllem11N  35741  pexmidlem8N  35752  cdlemftr3  36340  dibelval3  36922  dibglbN  36941  dicelval3  36955  dihglbcpreN  37075  dihglb2  37117  dihjatcclem4  37196  mapdordlem2  37412  mapdrvallem2  37420  mapdpglem3  37450  hdmapglem7a  37702  rp-isfinite5  38357  rp-isfinite6  38358  relintabex  38381  elintima  38439  iunrelexpuztr  38505  cotrclrcl  38528  neik0pk1imk0  38839  ntrneineine0lem  38875  ntrneineine1lem  38876  ntrneiel2  38878  rexbidar  39142  onfrALTlem5  39249  onfrALTlem2  39253  onfrALTlem1  39255  onfrALTlem5VD  39609  onfrALTlem2VD  39613  onfrALTlem1VD  39614  chordthmALT  39657  rspcegf  39670  cncmpmax  39679  rfcnnnub  39683  inn0f  39729  nssrex  39747  eluni2f  39772  eliin2f  39773  suprnmpt  39838  founiiun0  39860  disjinfi  39863  fvelima2  39952  ssfiunibd  39998  infrpge  40041  fsumiunss  40281  islpcn  40345  lptre2pt  40346  stoweidlem14  40704  stoweidlem34  40724  stoweidlem35  40725  stoweidlem43  40733  stoweidlem44  40734  stoweidlem50  40740  stoweidlem54  40744  stoweidlem56  40746  stoweidlem59  40749  stoweidlem60  40750  fourier2  40917  qndenserrnbllem  40987  qndenserrn  40992  sge0rpcpnf  41111  hoidmvval0b  41280  hoiqssbllem3  41314  2rmoswap  41690  opeliun2xp  42673  setrec1lem3  42998
  Copyright terms: Public domain W3C validator