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

Definition df-rex 2815
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  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)

Detailed syntax breakdown of Definition df-rex
StepHypRef Expression
1 wph . . 3  wff  ph
2 vx . . 3  setvar  x
3 cA . . 3  class  A
41, 2, 3wrex 2810 . 2  wff  E. x  e.  A  ph
52cv 1373 . . . . 5  class  x
65, 3wcel 1762 . . . 4  wff  x  e.  A
76, 1wa 369 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wex 1591 . 2  wff  E. x
( x  e.  A  /\  ph )
94, 8wb 184 1  wff  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
Colors of variables: wff setvar class
This definition is referenced by:  ralnex  2905  rexnalOLD  2908  rexex  2916  rspe  2917  rsp2eOLD  2919  nfre1  2920  reximi2  2926  reximdv2  2929  r19.23t  2936  rexbii2  2958  rexbida  2963  rexbidv2  2964  r2exfOLD  2979  risset  2982  r19.41  3008  reean  3023  rexeqf  3050  reu5  3072  rmo5  3075  cbvrexdva2  3088  rexv  3123  2gencl  3139  3gencl  3140  rspce  3204  ceqsrexv  3232  rexab  3261  rexab2  3265  rexrab2  3266  morex  3282  reu2  3286  reu6  3287  reu3  3288  2reuswap  3301  2reu5lem3  3306  2reu5  3307  rexun  3679  reuss2  3773  reuun2  3776  reupick  3777  reupick3  3778  reximdva0  3791  rabn0  3800  r19.2z  3912  r19.2zb  3913  rexsns  4055  rexsnsOLD  4056  exsnrex  4060  dfuni2  4242  eluni2  4244  elunirab  4252  iuncom4  4328  iunxiun  4403  intexrab  4601  reusv5OLD  4652  elxp2  5012  opeliunxp  5045  xpiundi  5048  xpiundir  5049  dmuni  5205  rnmpt  5241  elrnmpt1  5244  elres  5302  dfima2  5332  dfima3  5333  elima2  5336  dfco2a  5500  imaco  5505  dffo4  6030  dffo5  6031  abrexco  6137  isomin  6214  zfrep6  6744  opabex3d  6754  opabex3  6755  abexssex  6758  abexex  6759  frxp  6885  rdglim2  7090  oarec  7203  oeeu  7244  mapsn  7452  mapsnen  7585  pssnn  7730  unblem2  7764  dffi2  7874  marypha2lem4  7889  marypha2  7890  zfregcl  8011  axinf2  8048  zfinf2  8050  rankuni  8272  scott0  8295  cp  8300  bnd2  8302  infpwfien  8434  aceq1  8489  dfac5lem2  8496  dfac5lem3  8497  dfac2  8502  kmlem3  8523  kmlem6  8526  kmlem8  8528  kmlem14  8534  infmap2  8589  ackbij2  8614  cfub  8620  cfval2  8631  cflim3  8633  cfss  8636  cfslb  8637  isf32lem9  8732  zorn2lem6  8872  iundom2g  8906  winalim2  9065  grothprim  9203  genpass  9378  nqpr  9383  1idpr  9398  ltexprlem4  9408  ltexprlem5  9409  reclem2pr  9417  axrrecex  9531  dedekind  9734  sup2  10490  infm3  10493  nnunb  10782  2rexuz  11124  nnwos  11140  xrsupsslem  11489  xrinfmsslem  11490  cshwsexa  12744  wwlktovfo  12848  maxprmfct  14104  vdwapun  14342  vdwmc  14346  vdwmc2  14347  ram0  14390  imasleval  14787  mreexexlem2d  14891  isssc  15041  drsdirfi  15416  dirge  15715  psgnunilem4  16313  odcau  16415  ablfac2  16925  lspprat  17577  lidlnz  17653  isbasis2g  19211  tgval2  19219  ntreq0  19339  neitr  19442  cmpfi  19669  is1stc2  19704  2ndcsb  19711  2ndcsep  19721  1stcelcls  19723  hausmapdom  19762  isfbas2  20066  fbssint  20069  isfil2  20087  elfg  20102  fgcl  20109  uffix2  20155  alexsubALTlem4  20280  lpbl  20736  metustexhalfOLD  20796  metustexhalf  20797  metuel2  20812  restmetu  20820  bcthlem5  21497  umgraex  23988  usgraedg4  24051  uvtx01vtx  24156  3v3e3cycl2  24328  wlknwwlknsur  24376  wlkiswwlksur  24383  wwlkextsur  24395  frisusgranb  24661  frgra3vlem2  24665  3vfriswmgralem  24668  frgrancvvdeqlemC  24704  usg2spot2nb  24730  ubthlem1  25450  axhcompl-zf  25579  isch3  25823  shne0i  26030  cnlnssadj  26663  2reuswap2  27051  rexunirn  27054  rmoxfrdOLD  27055  rmoxfrd  27056  abrexdomjm  27067  abrexexd  27069  fpwrelmapffslem  27215  ishashinf  27262  ordtconlem1  27530  ddemeas  27836  eulerpartlemgvv  27943  erdszelem10  28272  ptpcon  28306  coep  28745  coepr  28746  dffr5  28747  dfpo2  28749  opelco3  28773  dfon2lem8  28787  brimg  29152  dfrdg4  29165  tfrqfree  29166  ellines  29367  neifg  29781  abrexdom  29813  prdstotbnd  29882  n0el  30193  prtlem17  30210  prter2  30215  rexbidar  30890  ssrexf  30923  rspcegf  30933  cncmpmax  30942  rfcnnnub  30946  suprnmpt  30986  ssfiunibd  31043  limcrecl  31128  islpcn  31138  lptre2pt  31139  stoweidlem14  31271  stoweidlem34  31291  stoweidlem35  31292  stoweidlem43  31300  stoweidlem44  31301  stoweidlem50  31307  stoweidlem54  31311  stoweidlem56  31313  stoweidlem59  31316  stoweidlem60  31317  fourier2  31485  2rmoswap  31613  opeliun2xp  31863  onfrALTlem5  32271  onfrALTlem2  32275  onfrALTlem1  32277  onfrALTlem5VD  32642  onfrALTlem2VD  32646  onfrALTlem1VD  32647  chordthmALT  32690  bnj168  32742  bnj956  32791  bnj1098  32798  bnj1143  32805  bnj1146  32806  bnj1185  32808  bnj1196  32809  bnj600  32933  bnj849  32939  bnj906  32944  bnj916  32947  bnj983  32965  bnj984  32966  bnj1083  32990  bnj1176  33017  bnj1186  33019  bnj1189  33021  bnj1228  33023  bnj1253  33029  bnj1398  33046  bnj1463  33067  bnj1312  33070  bnj1514  33075  bj-rexvwv  33400  bj-rexcom4  33403  bj-snglc  33485  bj-snglss  33486  bj-finsumval0  33612  islshpat  33691  lsat0cv  33707  lshpsmreu  33783  atex  34079  islpln5  34208  islvol5  34252  pmapglb  34443  pmapglb2N  34444  pmapglb2xN  34445  elpaddn0  34473  pmapjat1  34526  polval2N  34579  osumcllem11N  34639  pexmidlem8N  34650  cdlemftr3  35238  dibelval3  35821  dibglbN  35840  dicelval3  35854  dihglbcpreN  35974  dihglb2  36016  dihjatcclem4  36095  mapdordlem2  36311  mapdrvallem2  36319  mapdpglem3  36349  hdmapglem7a  36604
  Copyright terms: Public domain W3C validator