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 3136
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 3135). (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 3131 . 2 wff 𝑥𝐴 𝜑
52cv 1537 . . . . 5 class 𝑥
65, 3wcel 2114 . . . 4 wff 𝑥𝐴
76, 1wa 399 . . 3 wff (𝑥𝐴𝜑)
87, 2wex 1781 . 2 wff 𝑥(𝑥𝐴𝜑)
94, 8wb 209 1 wff (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  ralnex  3224  rexex  3228  reximi2  3232  rexbii2  3233  rexcom4  3237  rexanidOLD  3241  risset  3253  reximdv2  3257  rexbidv2  3281  rspe  3290  nfre1  3292  reximd2a  3298  r19.23t  3299  rexbida  3304  ralrexbid  3308  r19.12  3310  r19.41v  3328  r19.41  3329  rexcom  3336  reeanlem  3346  rexeqf  3379  reu5  3403  rmo5  3407  cbvrexvw  3425  cbvrexdva2  3432  cbvrexdva2OLD  3433  rexv  3495  2gencl  3510  3gencl  3511  rspce  3587  ceqsrexv  3624  rexab  3661  rexab2  3666  rexab2OLD  3667  rexrab2  3668  morex  3685  reu2  3691  reu6  3692  reu3  3693  2reuswap  3712  2reuswap2  3713  2reu5lem3  3723  2reu5  3724  2rmoswap  3727  ssrexf  4006  rexdifi  4097  rexun  4141  reuss2  4257  reuun2  4260  reupick  4261  reupick3  4262  euelss  4264  reximdva0  4284  n0rex  4286  n0el  4293  r19.2z  4412  r19.2zb  4413  rexsns  4583  exsnrex  4592  dfuni2  4815  eluni2  4817  elunirab  4829  iuncom4  4902  iunxiun  4994  axrep6  5173  axsepgfromrep  5177  intexrab  5219  opeliunxp  5596  xpiundi  5599  xpiundir  5600  ssrelrn  5740  dmuni  5760  rnmpt  5804  elrnmpt1  5807  dfima2  5909  dfima3  5910  elima2  5913  dfco2a  6077  imaco  6082  elsnxp  6120  dffo4  6851  dffo5  6852  abrexco  6986  isomin  7074  zfrep6  7642  opabex3d  7652  opabex3rd  7653  opabex3  7654  abexssex  7657  abexex  7658  frxp  7807  dfrecs3  7996  rdglim2  8055  oarec  8175  oeeu  8216  mapsnd  8437  mapsnend  8575  pssnn  8724  unblem2  8759  dffi2  8875  marypha2lem4  8890  marypha2  8891  zfregcl  9046  axinf2  9091  zfinf2  9093  rankuni  9280  scott0  9303  cp  9308  bnd2  9310  infpwfien  9477  aceq1  9532  dfac5lem2  9539  dfac5lem3  9540  dfac2b  9545  kmlem3  9567  kmlem6  9570  kmlem8  9572  kmlem14  9578  infmap2  9629  ackbij2  9654  cfub  9660  cfval2  9671  cflim3  9673  cfss  9676  cfslb  9677  isf32lem9  9772  zorn2lem6  9912  iundom2g  9951  winalim2  10107  grothprim  10245  genpass  10420  nqpr  10425  1idpr  10440  ltexprlem4  10450  ltexprlem5  10451  reclem2pr  10459  axrrecex  10574  dedekind  10792  sup2  11584  infm3  11587  nnunb  11881  2rexuz  12288  nnwos  12303  xrsupsslem  12688  xrinfmsslem  12689  hashgt23el  13781  ishashinf  13817  cshwsexa  14177  wwlktovfo  14313  maxprmfct  16042  vdwapun  16299  vdwmc  16303  vdwmc2  16304  ram0  16347  imasleval  16805  mreexexlem2d  16907  dfiso2  17033  isssc  17081  drsdirfi  17539  dirge  17838  pwmnd  18093  psgnunilem4  18616  odcau  18720  ablfac2  19202  lspprat  19916  lidlnz  19992  isbasis2g  21551  tgval2  21559  ntreq0  21680  neitr  21783  cmpfi  22011  is1stc2  22045  2ndcsb  22052  2ndcsep  22062  1stcelcls  22064  hausmapdom  22103  isfbas2  22438  fbssint  22441  isfil2  22459  elfg  22474  fgcl  22481  uffix2  22527  alexsubALTlem4  22653  lpbl  23108  metustexhalf  23161  metuel2  23170  restmetu  23175  bcthlem5  23930  upgrex  26883  uvtx01vtx  27185  uhgrvd00  27322  wlkswwlksf1o  27663  wwlksnextsurj  27684  frcond3  28052  frgr3vlem2  28057  3vfriswmgrlem  28060  frgrncvvdeqlem9  28090  ubthlem1  28651  axhcompl-zf  28779  isch3  29022  shne0i  29229  cnlnssadj  29861  reuxfrdf  30260  rexunirn  30261  rmoxfrd  30262  dmrab  30265  abrexdomjm  30273  abrexexd  30275  iunrnmptss  30324  1stpreimas  30449  fpwrelmapffslem  30478  qsxpid  30959  krull  31022  zarclsint  31194  ordtconnlem1  31241  ddemeas  31569  omssubaddlem  31631  omssubadd  31632  eulerpartlemgvv  31708  tgoldbachgt  32008  bnj168  32074  bnj956  32122  bnj1098  32129  bnj1143  32136  bnj1146  32137  bnj1185  32139  bnj1196  32140  bnj600  32265  bnj849  32271  bnj906  32276  bnj916  32279  bnj983  32297  bnj984  32298  bnj1083  32324  bnj1176  32351  bnj1186  32353  bnj1189  32355  bnj1228  32357  bnj1253  32363  bnj1398  32380  bnj1463  32401  bnj1312  32404  bnj1514  32409  exdifsn  32419  lfuhgr3  32440  cusgredgex  32442  loop1cycl  32458  erdszelem10  32521  ptpconn  32554  coep  33061  coepr  33062  dffr5  33063  dfpo2  33065  opelco3  33092  dfon2lem8  33109  brimg  33472  dfrecs2  33485  dfrdg4  33486  ellines  33687  neifg  33793  bj-rexvw  34281  bj-snglc  34366  bj-snglss  34367  bj-rest10  34464  bj-restn0  34466  bj-restpw  34468  bj-rest0  34469  bj-restb  34470  bj-restuni  34473  bj-dfmpoa  34494  bj-finsumval0  34661  rnmptsn  34713  f1omptsnlem  34714  mptsnunlem  34716  topdifinffinlem  34725  isbasisrelowllem1  34733  isbasisrelowllem2  34734  relowlpssretop  34742  fvineqsneq  34790  pibt2  34795  poimirlem30  35045  abrexdom  35126  prdstotbnd  35190  eldmqsres2  35662  exanres  35670  rncnvepres  35679  rnxrnres  35765  1cossres  35792  eldm1cossres  35818  eldmqs1cossres  36011  prtlem17  36130  prter2  36135  islshpat  36271  lsat0cv  36287  lshpsmreu  36363  atex  36660  islpln5  36789  islvol5  36833  pmapglb  37024  pmapglb2N  37025  pmapglb2xN  37026  elpaddn0  37054  pmapjat1  37107  polval2N  37160  osumcllem11N  37220  pexmidlem8N  37231  cdlemftr3  37819  dibelval3  38401  dibglbN  38420  dicelval3  38434  dihglbcpreN  38554  dihglb2  38596  dihjatcclem4  38675  mapdordlem2  38891  mapdrvallem2  38899  mapdpglem3  38929  hdmapglem7a  39181  imaopab  39360  prjspeclsp  39536  rp-isfinite5  40155  rp-isfinite6  40156  elintima  40284  iunrelexpuztr  40350  cotrclrcl  40373  neik0pk1imk0  40683  ntrneineine0lem  40719  ntrneineine1lem  40720  ntrneiel2  40722  cpcolld  40900  expandrexn  40933  ismnuprim  40936  rr-grothprimbi  40937  rr-groth  40941  rexbidar  41084  onfrALTlem5  41182  onfrALTlem2  41186  onfrALTlem1  41188  onfrALTlem5VD  41525  onfrALTlem2VD  41529  onfrALTlem1VD  41530  chordthmALT  41573  rspcegf  41586  cncmpmax  41595  rfcnnnub  41599  inn0f  41641  nssrex  41657  eluni2f  41675  eliin2f  41676  suprnmpt  41735  founiiun0  41755  disjinfi  41758  fvelima2  41836  ssfiunibd  41880  infrpge  41922  fsumiunss  42156  islpcn  42220  lptre2pt  42221  stoweidlem14  42595  stoweidlem34  42615  stoweidlem35  42616  stoweidlem43  42624  stoweidlem44  42625  stoweidlem50  42631  stoweidlem54  42635  stoweidlem56  42637  stoweidlem59  42640  stoweidlem60  42641  fourier2  42808  qndenserrnbllem  42875  qndenserrn  42880  sge0rpcpnf  42999  hoidmvval0b  43168  hoiqssbllem3  43202  imasetpreimafvbijlemfv1  43859  nfermltl8rev  44199  nfermltl2rev  44200  nfermltlrev  44201  nn0mnd  44378  opeliun2xp  44673  setrec1lem3  45158
  Copyright terms: Public domain W3C validator