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

Definition df-rex 2738
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 2733 . 2  wff  E. x  e.  A  ph
52cv 1398 . . . . 5  class  x
65, 3wcel 1826 . . . 4  wff  x  e.  A
76, 1wa 367 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wex 1620 . 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  2828  rexnalOLD  2831  rexex  2839  rspe  2840  rsp2eOLD  2842  nfre1  2843  reximi2  2849  reximd2a  2852  reximdv2  2853  r19.23t  2860  rexbii2  2882  rexbida  2888  rexbidv2  2889  r2exfOLD  2904  risset  2907  r19.41v  2934  r19.41  2935  reean  2949  rexeqf  2976  reu5  2998  rmo5  3001  cbvrexdva2  3014  rexv  3049  2gencl  3065  3gencl  3066  rspce  3130  ceqsrexv  3158  rexab  3187  rexab2  3191  rexrab2  3192  morex  3208  reu2  3212  reu6  3213  reu3  3214  2reuswap  3227  2reu5lem3  3232  2reu5  3233  ssrexf  3477  rexun  3598  reuss2  3703  reuun2  3706  reupick  3707  reupick3  3708  euelss  3710  reximdva0  3723  rabn0  3732  r19.2z  3834  r19.2zb  3835  rexsns  3977  rexsnsOLD  3978  exsnrex  3982  dfuni2  4165  eluni2  4167  elunirab  4175  iuncom4  4251  iunxiun  4329  intexrab  4524  elxp2  4931  opeliunxp  4965  xpiundi  4968  xpiundir  4969  dmuni  5125  rnmpt  5161  elrnmpt1  5164  elres  5221  dfima2  5251  dfima3  5252  elima2  5255  dfco2a  5415  imaco  5420  dffo4  5949  dffo5  5950  abrexco  6057  isomin  6134  zfrep6  6667  opabex3d  6677  opabex3  6678  abexssex  6681  abexex  6682  frxp  6809  rdglim2  7016  oarec  7129  oeeu  7170  mapsn  7379  mapsnen  7512  pssnn  7654  unblem2  7688  dffi2  7798  marypha2lem4  7813  marypha2  7814  zfregcl  7935  axinf2  7971  zfinf2  7973  rankuni  8194  scott0  8217  cp  8222  bnd2  8224  infpwfien  8356  aceq1  8411  dfac5lem2  8418  dfac5lem3  8419  dfac2  8424  kmlem3  8445  kmlem6  8448  kmlem8  8450  kmlem14  8456  infmap2  8511  ackbij2  8536  cfub  8542  cfval2  8553  cflim3  8555  cfss  8558  cfslb  8559  isf32lem9  8654  zorn2lem6  8794  iundom2g  8828  winalim2  8985  grothprim  9123  genpass  9298  nqpr  9303  1idpr  9318  ltexprlem4  9328  ltexprlem5  9329  reclem2pr  9337  axrrecex  9451  dedekind  9655  sup2  10415  infm3  10418  nnunb  10708  2rexuz  11053  nnwos  11068  xrsupsslem  11419  xrinfmsslem  11420  cshwsexa  12703  wwlktovfo  12807  maxprmfct  14256  vdwapun  14494  vdwmc  14498  vdwmc2  14499  ram0  14542  imasleval  14948  mreexexlem2d  15052  dfiso2  15178  isssc  15226  drsdirfi  15684  dirge  15984  psgnunilem4  16639  odcau  16741  ablfac2  17253  lspprat  17912  lidlnz  17989  isbasis2g  19534  tgval2  19542  ntreq0  19664  neitr  19767  cmpfi  19994  is1stc2  20028  2ndcsb  20035  2ndcsep  20045  1stcelcls  20047  hausmapdom  20086  isfbas2  20421  fbssint  20424  isfil2  20442  elfg  20457  fgcl  20464  uffix2  20510  alexsubALTlem4  20635  lpbl  21091  metustexhalfOLD  21151  metustexhalf  21152  metuel2  21167  restmetu  21175  bcthlem5  21852  umgraex  24444  usgraedg4  24508  uvtx01vtx  24613  3v3e3cycl2  24785  wlknwwlknsur  24833  wlkiswwlksur  24840  wwlkextsur  24852  frisusgranb  25118  frgra3vlem2  25122  3vfriswmgralem  25125  frgrancvvdeqlemC  25160  usg2spot2nb  25186  ubthlem1  25903  axhcompl-zf  26032  isch3  26276  shne0i  26483  cnlnssadj  27115  2reuswap2  27504  rexunirn  27507  rmoxfrdOLD  27508  rmoxfrd  27509  abrexdomjm  27523  abrexexd  27525  iunxsngf  27553  elsnxp  27603  1stpreimas  27671  fpwrelmapffslem  27705  ishashinf  27759  ordtconlem1  28060  ddemeas  28364  omssubaddlem  28426  omssubadd  28427  eulerpartlemgvv  28498  erdszelem10  28833  ptpcon  28867  coep  29346  coepr  29347  dffr5  29348  dfpo2  29350  opelco3  29373  dfon2lem8  29387  brimg  29740  dfrdg4  29753  tfrqfree  29754  ellines  29955  neifg  30355  abrexdom  30387  prdstotbnd  30456  n0el  30766  prtlem17  30783  prter2  30788  rexbidar  31523  rspcegf  31565  cncmpmax  31574  rfcnnnub  31578  suprnmpt  31618  ssfiunibd  31675  islpcn  31811  lptre2pt  31812  stoweidlem14  31962  stoweidlem34  31982  stoweidlem35  31983  stoweidlem43  31991  stoweidlem44  31992  stoweidlem50  31998  stoweidlem54  32002  stoweidlem56  32004  stoweidlem59  32007  stoweidlem60  32008  fourier2  32176  2rmoswap  32355  opeliun2xp  33122  onfrALTlem5  33654  onfrALTlem2  33658  onfrALTlem1  33660  onfrALTlem5VD  34032  onfrALTlem2VD  34036  onfrALTlem1VD  34037  chordthmALT  34080  bnj168  34132  bnj956  34182  bnj1098  34189  bnj1143  34196  bnj1146  34197  bnj1185  34199  bnj1196  34200  bnj600  34324  bnj849  34330  bnj906  34335  bnj916  34338  bnj983  34356  bnj984  34357  bnj1083  34381  bnj1176  34408  bnj1186  34410  bnj1189  34412  bnj1228  34414  bnj1253  34420  bnj1398  34437  bnj1463  34458  bnj1312  34461  bnj1514  34466  bj-rexvwv  34789  bj-rexcom4  34792  bj-snglc  34875  bj-snglss  34876  bj-finsumval0  35010  islshpat  35155  lsat0cv  35171  lshpsmreu  35247  atex  35543  islpln5  35672  islvol5  35716  pmapglb  35907  pmapglb2N  35908  pmapglb2xN  35909  elpaddn0  35937  pmapjat1  35990  polval2N  36043  osumcllem11N  36103  pexmidlem8N  36114  cdlemftr3  36704  dibelval3  37287  dibglbN  37306  dicelval3  37320  dihglbcpreN  37440  dihglb2  37482  dihjatcclem4  37561  mapdordlem2  37777  mapdrvallem2  37785  mapdpglem3  37815  hdmapglem7a  38070  rp-isfinite5  38172  rp-isfinite6  38173  elintima  38195  iunrelexpuztr  38224  cotrclrcl  38250
  Copyright terms: Public domain W3C validator