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 3048
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 3043 . 2 wff 𝑥𝐴 𝜑
52cv 1623 . . . . 5 class 𝑥
65, 3wcel 2131 . . . 4 wff 𝑥𝐴
76, 1wa 383 . . 3 wff (𝑥𝐴𝜑)
87, 2wex 1845 . 2 wff 𝑥(𝑥𝐴𝜑)
94, 8wb 196 1 wff (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  ralnex  3122  ralnexOLD  3123  rexex  3132  rspe  3133  nfre1  3135  reximi2  3140  reximd2a  3143  reximdv2  3144  r19.23t  3151  rexbii2  3169  rexbida  3177  rexbidv2  3178  risset  3192  r19.41v  3219  r19.41  3220  reean  3236  rexeqf  3266  reu5  3290  rmo5  3293  cbvrexdva2  3307  rexv  3352  2gencl  3368  3gencl  3369  rspce  3436  ceqsrexv  3467  rexab  3502  rexab2  3506  rexrab2  3507  morex  3523  reu2  3527  reu6  3528  reu3  3529  2reuswap  3543  2reu5lem3  3548  2reu5  3549  ssrexf  3798  rexun  3928  reuss2  4042  reuun2  4045  reupick  4046  reupick3  4047  euelss  4049  reximdva0  4068  n0rex  4070  n0el  4075  rabn0OLD  4094  r19.2z  4196  r19.2zb  4197  rexsns  4353  exsnrex  4357  dfuni2  4582  eluni2  4584  elunirab  4592  iuncom4  4672  iunxiun  4752  intexrab  4964  elxp2OLD  5282  opeliunxp  5319  xpiundi  5322  xpiundir  5323  ssrelrn  5462  dmuni  5481  rnmpt  5518  elrnmpt1  5521  elres  5585  dfima2  5618  dfima3  5619  elima2  5622  dfco2a  5788  imaco  5793  elsnxp  5830  elsnxpOLD  5831  dffo4  6530  dffo5  6531  abrexco  6657  isomin  6742  zfrep6  7291  opabex3d  7302  opabex3  7303  abexssex  7306  abexex  7308  frxp  7447  dfrecs3  7630  rdglim2  7689  oarec  7803  oeeu  7844  mapsn  8057  mapsnen  8192  pssnn  8335  unblem2  8370  dffi2  8486  marypha2lem4  8501  marypha2  8502  zfregcl  8656  axinf2  8702  zfinf2  8704  rankuni  8891  scott0  8914  cp  8919  bnd2  8921  infpwfien  9067  aceq1  9122  dfac5lem2  9129  dfac5lem3  9130  dfac2b  9135  dfac2OLD  9137  kmlem3  9158  kmlem6  9161  kmlem8  9163  kmlem14  9169  infmap2  9224  ackbij2  9249  cfub  9255  cfval2  9266  cflim3  9268  cfss  9271  cfslb  9272  isf32lem9  9367  zorn2lem6  9507  iundom2g  9546  winalim2  9702  grothprim  9840  genpass  10015  nqpr  10020  1idpr  10035  ltexprlem4  10045  ltexprlem5  10046  reclem2pr  10054  axrrecex  10168  dedekind  10384  sup2  11163  infm3  11166  nnunb  11472  2rexuz  11925  nnwos  11940  xrsupsslem  12322  xrinfmsslem  12323  ishashinf  13431  cshwsexa  13762  wwlktovfo  13894  ncoprmgcdne1b  15557  maxprmfct  15615  vdwapun  15872  vdwmc  15876  vdwmc2  15877  ram0  15920  imasleval  16395  mreexexlem2d  16499  dfiso2  16625  isssc  16673  drsdirfi  17131  dirge  17430  psgnunilem4  18109  odcau  18211  ablfac2  18680  lspprat  19347  lidlnz  19422  isbasis2g  20946  tgval2  20954  ntreq0  21075  neitr  21178  cmpfi  21405  is1stc2  21439  2ndcsb  21446  2ndcsep  21456  1stcelcls  21458  hausmapdom  21497  isfbas2  21832  fbssint  21835  isfil2  21853  elfg  21868  fgcl  21875  uffix2  21921  alexsubALTlem4  22047  lpbl  22501  metustexhalf  22554  metuel2  22563  restmetu  22568  bcthlem5  23317  upgrex  26178  uvtx01vtx  26492  uvtxa01vtx0OLD  26494  uhgrvd00  26632  wlkpwwlkf1ouspgr  26980  wlknwwlksnsur  26991  wlkwwlksur  26998  wwlksnextsur  27010  frcond3  27415  frgr3vlem2  27420  3vfriswmgrlem  27423  frgrncvvdeqlem9  27453  ubthlem1  28027  axhcompl-zf  28156  isch3  28399  shne0i  28608  cnlnssadj  29240  2reuswap2  29628  rexunirn  29631  rmoxfrdOLD  29632  rmoxfrd  29633  abrexdomjm  29644  abrexexd  29646  1stpreimas  29784  fpwrelmapffslem  29808  ordtconnlem1  30271  ddemeas  30600  omssubaddlem  30662  omssubadd  30663  eulerpartlemgvv  30739  tgoldbachgt  31042  bnj168  31097  bnj956  31146  bnj1098  31153  bnj1143  31160  bnj1146  31161  bnj1185  31163  bnj1196  31164  bnj600  31288  bnj849  31294  bnj906  31299  bnj916  31302  bnj983  31320  bnj984  31321  bnj1083  31345  bnj1176  31372  bnj1186  31374  bnj1189  31376  bnj1228  31378  bnj1253  31384  bnj1398  31401  bnj1463  31422  bnj1312  31425  bnj1514  31430  erdszelem10  31481  ptpconn  31514  coep  31940  coepr  31941  dffr5  31942  dfpo2  31944  opelco3  31975  dfon2lem8  31992  brimg  32342  dfrecs2  32355  dfrdg4  32356  ellines  32557  neifg  32664  bj-rexvwv  33164  bj-rexcom4  33167  bj-snglc  33255  bj-snglss  33256  bj-rest10  33339  bj-restn0  33341  bj-restpw  33343  bj-rest0  33344  bj-restb  33345  bj-restuni  33348  bj-dfmpt2a  33369  bj-finsumval0  33450  rnmptsn  33485  f1omptsnlem  33486  mptsnunlem  33488  topdifinffinlem  33498  isbasisrelowllem1  33506  isbasisrelowllem2  33507  relowlpssretop  33515  poimirlem30  33744  abrexdom  33830  prdstotbnd  33898  eldmqsres2  34368  exanres  34379  rncnvepres  34389  rnxrnres  34472  1cossres  34499  eldm1cossres  34525  prtlem17  34657  prter2  34662  islshpat  34799  lsat0cv  34815  lshpsmreu  34891  atex  35187  islpln5  35316  islvol5  35360  pmapglb  35551  pmapglb2N  35552  pmapglb2xN  35553  elpaddn0  35581  pmapjat1  35634  polval2N  35687  osumcllem11N  35747  pexmidlem8N  35758  cdlemftr3  36347  dibelval3  36930  dibglbN  36949  dicelval3  36963  dihglbcpreN  37083  dihglb2  37125  dihjatcclem4  37204  mapdordlem2  37420  mapdrvallem2  37428  mapdpglem3  37458  hdmapglem7a  37713  rp-isfinite5  38357  rp-isfinite6  38358  relintabex  38381  elintima  38439  iunrelexpuztr  38505  cotrclrcl  38528  neik0pk1imk0  38839  ntrneineine0lem  38875  ntrneineine1lem  38876  ntrneiel2  38878  rexbidar  39144  onfrALTlem5  39251  onfrALTlem2  39255  onfrALTlem1  39257  onfrALTlem5VD  39612  onfrALTlem2VD  39616  onfrALTlem1VD  39617  chordthmALT  39660  rspcegf  39673  cncmpmax  39682  rfcnnnub  39686  inn0f  39733  nssrex  39751  eluni2f  39777  eliin2f  39778  suprnmpt  39846  founiiun0  39868  disjinfi  39871  mapsnd  39879  mapsnend  39882  fvelima2  39966  ssfiunibd  40014  infrpge  40057  fsumiunss  40302  islpcn  40366  lptre2pt  40367  stoweidlem14  40726  stoweidlem34  40746  stoweidlem35  40747  stoweidlem43  40755  stoweidlem44  40756  stoweidlem50  40762  stoweidlem54  40766  stoweidlem56  40768  stoweidlem59  40771  stoweidlem60  40772  fourier2  40939  qndenserrnbllem  41009  qndenserrn  41014  sge0rpcpnf  41133  hoidmvval0b  41302  hoiqssbllem3  41336  2rmoswap  41682  opeliun2xp  42613  setrec1lem3  42938
  Copyright terms: Public domain W3C validator