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 2947
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 2942 . 2 wff 𝑥𝐴 𝜑
52cv 1522 . . . . 5 class 𝑥
65, 3wcel 2030 . . . 4 wff 𝑥𝐴
76, 1wa 383 . . 3 wff (𝑥𝐴𝜑)
87, 2wex 1744 . 2 wff 𝑥(𝑥𝐴𝜑)
94, 8wb 196 1 wff (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  ralnex  3021  ralnexOLD  3022  rexex  3031  rspe  3032  nfre1  3034  reximi2  3039  reximd2a  3042  reximdv2  3043  r19.23t  3050  rexbii2  3068  rexbida  3076  rexbidv2  3077  risset  3091  r19.41v  3118  r19.41  3119  reean  3135  rexeqf  3165  reu5  3189  rmo5  3192  cbvrexdva2  3206  rexv  3251  2gencl  3267  3gencl  3268  rspce  3335  ceqsrexv  3367  rexab  3402  rexab2  3406  rexrab2  3407  morex  3423  reu2  3427  reu6  3428  reu3  3429  2reuswap  3443  2reu5lem3  3448  2reu5  3449  ssrexf  3698  rexun  3826  reuss2  3940  reuun2  3943  reupick  3944  reupick3  3945  euelss  3947  reximdva0  3966  n0rex  3968  n0el  3973  rabn0OLD  3992  r19.2z  4093  r19.2zb  4094  rexsns  4249  exsnrex  4253  dfuni2  4470  eluni2  4472  elunirab  4480  iuncom4  4560  iunxiun  4640  intexrab  4853  elxp2OLD  5167  opeliunxp  5204  xpiundi  5207  xpiundir  5208  ssrelrn  5347  dmuni  5366  rnmpt  5403  elrnmpt1  5406  elres  5470  dfima2  5503  dfima3  5504  elima2  5507  dfco2a  5673  imaco  5678  elsnxp  5715  elsnxpOLD  5716  dffo4  6415  dffo5  6416  abrexco  6542  isomin  6627  zfrep6  7176  opabex3d  7187  opabex3  7188  abexssex  7191  abexex  7193  frxp  7332  dfrecs3  7514  rdglim2  7573  oarec  7687  oeeu  7728  mapsn  7941  mapsnen  8076  pssnn  8219  unblem2  8254  dffi2  8370  marypha2lem4  8385  marypha2  8386  zfregcl  8540  axinf2  8575  zfinf2  8577  rankuni  8764  scott0  8787  cp  8792  bnd2  8794  infpwfien  8923  aceq1  8978  dfac5lem2  8985  dfac5lem3  8986  dfac2  8991  kmlem3  9012  kmlem6  9015  kmlem8  9017  kmlem14  9023  infmap2  9078  ackbij2  9103  cfub  9109  cfval2  9120  cflim3  9122  cfss  9125  cfslb  9126  isf32lem9  9221  zorn2lem6  9361  iundom2g  9400  winalim2  9556  grothprim  9694  genpass  9869  nqpr  9874  1idpr  9889  ltexprlem4  9899  ltexprlem5  9900  reclem2pr  9908  axrrecex  10022  dedekind  10238  sup2  11017  infm3  11020  nnunb  11326  2rexuz  11778  nnwos  11793  xrsupsslem  12175  xrinfmsslem  12176  ishashinf  13285  cshwsexa  13616  wwlktovfo  13747  ncoprmgcdne1b  15410  maxprmfct  15468  vdwapun  15725  vdwmc  15729  vdwmc2  15730  ram0  15773  imasleval  16248  mreexexlem2d  16352  dfiso2  16479  isssc  16527  drsdirfi  16985  dirge  17284  psgnunilem4  17963  odcau  18065  ablfac2  18534  lspprat  19201  lidlnz  19276  isbasis2g  20800  tgval2  20808  ntreq0  20929  neitr  21032  cmpfi  21259  is1stc2  21293  2ndcsb  21300  2ndcsep  21310  1stcelcls  21312  hausmapdom  21351  isfbas2  21686  fbssint  21689  isfil2  21707  elfg  21722  fgcl  21729  uffix2  21775  alexsubALTlem4  21901  lpbl  22355  metustexhalf  22408  metuel2  22417  restmetu  22422  bcthlem5  23171  upgrex  26032  uvtx01vtx  26346  uvtxa01vtx0OLD  26348  uhgrvd00  26486  wlkpwwlkf1ouspgr  26833  wlknwwlksnsur  26844  wlkwwlksur  26851  wwlksnextsur  26863  frcond3  27249  frgr3vlem2  27254  3vfriswmgrlem  27257  frgrncvvdeqlem9  27287  ubthlem1  27854  axhcompl-zf  27983  isch3  28226  shne0i  28435  cnlnssadj  29067  2reuswap2  29455  rexunirn  29458  rmoxfrdOLD  29459  rmoxfrd  29460  abrexdomjm  29471  abrexexd  29473  1stpreimas  29611  fpwrelmapffslem  29635  ordtconnlem1  30098  ddemeas  30427  omssubaddlem  30489  omssubadd  30490  eulerpartlemgvv  30566  tgoldbachgt  30869  bnj168  30924  bnj956  30973  bnj1098  30980  bnj1143  30987  bnj1146  30988  bnj1185  30990  bnj1196  30991  bnj600  31115  bnj849  31121  bnj906  31126  bnj916  31129  bnj983  31147  bnj984  31148  bnj1083  31172  bnj1176  31199  bnj1186  31201  bnj1189  31203  bnj1228  31205  bnj1253  31211  bnj1398  31228  bnj1463  31249  bnj1312  31252  bnj1514  31257  erdszelem10  31308  ptpconn  31341  coep  31767  coepr  31768  dffr5  31769  dfpo2  31771  opelco3  31802  dfon2lem8  31819  brimg  32169  dfrecs2  32182  dfrdg4  32183  ellines  32384  neifg  32491  bj-rexvwv  32991  bj-rexcom4  32994  bj-snglc  33082  bj-snglss  33083  bj-rest10  33166  bj-restn0  33168  bj-restpw  33170  bj-rest0  33171  bj-restb  33172  bj-restuni  33175  bj-dfmpt2a  33196  bj-finsumval0  33277  rnmptsn  33312  f1omptsnlem  33313  mptsnunlem  33315  topdifinffinlem  33325  isbasisrelowllem1  33333  isbasisrelowllem2  33334  relowlpssretop  33342  poimirlem30  33569  abrexdom  33655  prdstotbnd  33723  eldmqsres2  34193  exanres  34204  rncnvepres  34214  rnxrnres  34297  1cossres  34324  eldm1cossres  34350  prtlem17  34480  prter2  34485  islshpat  34622  lsat0cv  34638  lshpsmreu  34714  atex  35010  islpln5  35139  islvol5  35183  pmapglb  35374  pmapglb2N  35375  pmapglb2xN  35376  elpaddn0  35404  pmapjat1  35457  polval2N  35510  osumcllem11N  35570  pexmidlem8N  35581  cdlemftr3  36170  dibelval3  36753  dibglbN  36772  dicelval3  36786  dihglbcpreN  36906  dihglb2  36948  dihjatcclem4  37027  mapdordlem2  37243  mapdrvallem2  37251  mapdpglem3  37281  hdmapglem7a  37536  rp-isfinite5  38180  rp-isfinite6  38181  relintabex  38204  elintima  38262  iunrelexpuztr  38328  cotrclrcl  38351  neik0pk1imk0  38662  ntrneineine0lem  38698  ntrneineine1lem  38699  ntrneiel2  38701  rexbidar  38967  onfrALTlem5  39074  onfrALTlem2  39078  onfrALTlem1  39080  onfrALTlem5VD  39435  onfrALTlem2VD  39439  onfrALTlem1VD  39440  chordthmALT  39483  rspcegf  39496  cncmpmax  39505  rfcnnnub  39509  inn0f  39556  nssrex  39574  eluni2f  39600  eliin2f  39601  suprnmpt  39669  founiiun0  39691  disjinfi  39694  mapsnd  39702  mapsnend  39705  fvelima2  39789  ssfiunibd  39837  infrpge  39880  fsumiunss  40125  islpcn  40189  lptre2pt  40190  stoweidlem14  40549  stoweidlem34  40569  stoweidlem35  40570  stoweidlem43  40578  stoweidlem44  40579  stoweidlem50  40585  stoweidlem54  40589  stoweidlem56  40591  stoweidlem59  40594  stoweidlem60  40595  fourier2  40762  qndenserrnbllem  40832  qndenserrn  40837  sge0rpcpnf  40956  hoidmvval0b  41125  hoiqssbllem3  41159  2rmoswap  41505  opeliun2xp  42436  setrec1lem3  42761
  Copyright terms: Public domain W3C validator