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

Definition df-rex 2788
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 2783 . 2  wff  E. x  e.  A  ph
52cv 1436 . . . . 5  class  x
65, 3wcel 1870 . . . 4  wff  x  e.  A
76, 1wa 370 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wex 1659 . 2  wff  E. x
( x  e.  A  /\  ph )
94, 8wb 187 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  2878  rexnalOLD  2881  rexex  2889  rspe  2890  rsp2eOLD  2892  nfre1  2893  reximi2  2899  reximd2a  2902  reximdv2  2903  r19.23t  2910  rexbii2  2932  rexbida  2941  rexbidv2  2942  r2exfOLD  2957  risset  2960  r19.41v  2987  r19.41  2988  reean  3002  rexeqf  3029  reu5  3051  rmo5  3054  cbvrexdva2  3067  rexv  3102  2gencl  3118  3gencl  3119  rspce  3183  ceqsrexv  3211  rexab  3240  rexab2  3244  rexrab2  3245  morex  3261  reu2  3265  reu6  3266  reu3  3267  2reuswap  3280  2reu5lem3  3285  2reu5  3286  ssrexf  3530  rexun  3652  reuss2  3759  reuun2  3762  reupick  3763  reupick3  3764  euelss  3766  reximdva0  3779  rabn0  3788  r19.2z  3892  r19.2zb  3893  rexsns  4035  rexsnsOLD  4036  exsnrex  4040  dfuni2  4224  eluni2  4226  elunirab  4234  iuncom4  4310  iunxiun  4388  intexrab  4584  elxp2  4872  opeliunxp  4906  xpiundi  4909  xpiundir  4910  dmuni  5064  rnmpt  5100  elrnmpt1  5103  elres  5160  dfima2  5190  dfima3  5191  elima2  5194  dfco2a  5355  imaco  5360  dffo4  6053  dffo5  6054  abrexco  6164  isomin  6243  zfrep6  6775  opabex3d  6785  opabex3  6786  abexssex  6789  abexex  6790  frxp  6917  dfrecs3  7099  rdglim2  7158  oarec  7271  oeeu  7312  mapsn  7521  mapsnen  7654  pssnn  7796  unblem2  7830  dffi2  7943  marypha2lem4  7958  marypha2  7959  zfregcl  8109  axinf2  8145  zfinf2  8147  rankuni  8333  scott0  8356  cp  8361  bnd2  8363  infpwfien  8491  aceq1  8546  dfac5lem2  8553  dfac5lem3  8554  dfac2  8559  kmlem3  8580  kmlem6  8583  kmlem8  8585  kmlem14  8591  infmap2  8646  ackbij2  8671  cfub  8677  cfval2  8688  cflim3  8690  cfss  8693  cfslb  8694  isf32lem9  8789  zorn2lem6  8929  iundom2g  8963  winalim2  9120  grothprim  9258  genpass  9433  nqpr  9438  1idpr  9453  ltexprlem4  9463  ltexprlem5  9464  reclem2pr  9472  axrrecex  9586  dedekind  9796  sup2  10565  infm3  10568  nnunb  10865  2rexuz  11211  nnwos  11226  xrsupsslem  11592  xrinfmsslem  11593  cshwsexa  12908  wwlktovfo  13012  maxprmfct  14623  ncoprmgcdne1b  14626  vdwapun  14887  vdwmc  14891  vdwmc2  14892  ram0  14943  imasleval  15398  mreexexlem2d  15502  dfiso2  15628  isssc  15676  drsdirfi  16134  dirge  16434  psgnunilem4  17089  odcau  17191  ablfac2  17657  lspprat  18311  lidlnz  18387  isbasis2g  19894  tgval2  19902  ntreq0  20024  neitr  20127  cmpfi  20354  is1stc2  20388  2ndcsb  20395  2ndcsep  20405  1stcelcls  20407  hausmapdom  20446  isfbas2  20781  fbssint  20784  isfil2  20802  elfg  20817  fgcl  20824  uffix2  20870  alexsubALTlem4  20996  lpbl  21449  metustexhalf  21502  metuel2  21511  restmetu  21516  bcthlem5  22189  umgraex  24896  usgraedg4  24960  uvtx01vtx  25065  3v3e3cycl2  25237  wlknwwlknsur  25285  wlkiswwlksur  25292  wwlkextsur  25304  frisusgranb  25570  frgra3vlem2  25574  3vfriswmgralem  25577  frgrancvvdeqlemC  25612  usg2spot2nb  25638  ubthlem1  26357  axhcompl-zf  26486  isch3  26729  shne0i  26936  cnlnssadj  27568  2reuswap2  27959  rexunirn  27962  rmoxfrdOLD  27963  rmoxfrd  27964  abrexdomjm  27977  abrexexd  27979  iunxsngf  28011  elsnxp  28063  1stpreimas  28126  fpwrelmapffslem  28160  ishashinf  28217  ordtconlem1  28569  ddemeas  28898  omssubaddlem  28960  omssubadd  28961  eulerpartlemgvv  29035  bnj168  29326  bnj956  29376  bnj1098  29383  bnj1143  29390  bnj1146  29391  bnj1185  29393  bnj1196  29394  bnj600  29518  bnj849  29524  bnj906  29529  bnj916  29532  bnj983  29550  bnj984  29551  bnj1083  29575  bnj1176  29602  bnj1186  29604  bnj1189  29606  bnj1228  29608  bnj1253  29614  bnj1398  29631  bnj1463  29652  bnj1312  29655  bnj1514  29660  erdszelem10  29711  ptpcon  29744  coep  30178  coepr  30179  dffr5  30180  dfpo2  30182  opelco3  30207  dfon2lem8  30223  brimg  30489  dfrecs2  30502  dfrdg4  30503  ellines  30704  neifg  30812  bj-rexvwv  31226  bj-rexcom4  31229  bj-snglc  31312  bj-snglss  31313  bj-finsumval0  31447  rnmptsn  31471  f1omptsnlem  31472  mptsnunlem  31474  topdifinffinlem  31484  isbasisrelowllem1  31492  isbasisrelowllem2  31493  relowlpssretop  31501  poimirlem30  31674  abrexdom  31761  prdstotbnd  31830  n0el  32139  prtlem17  32156  prter2  32161  islshpat  32292  lsat0cv  32308  lshpsmreu  32384  atex  32680  islpln5  32809  islvol5  32853  pmapglb  33044  pmapglb2N  33045  pmapglb2xN  33046  elpaddn0  33074  pmapjat1  33127  polval2N  33180  osumcllem11N  33240  pexmidlem8N  33251  cdlemftr3  33841  dibelval3  34424  dibglbN  34443  dicelval3  34457  dihglbcpreN  34577  dihglb2  34619  dihjatcclem4  34698  mapdordlem2  34914  mapdrvallem2  34922  mapdpglem3  34952  hdmapglem7a  35207  rp-isfinite5  35861  rp-isfinite6  35862  elintima  35884  iunrelexpuztr  35950  cotrclrcl  35973  rexbidar  36436  onfrALTlem5  36545  onfrALTlem2  36549  onfrALTlem1  36551  onfrALTlem5VD  36922  onfrALTlem2VD  36926  onfrALTlem1VD  36927  chordthmALT  36970  rspcegf  36984  cncmpmax  36993  rfcnnnub  36997  suprnmpt  37061  founiiun0  37088  disjinfi  37091  ssfiunibd  37136  fsumiunss  37229  islpcn  37291  lptre2pt  37292  stoweidlem14  37443  stoweidlem34  37464  stoweidlem35  37465  stoweidlem43  37473  stoweidlem44  37474  stoweidlem50  37480  stoweidlem54  37484  stoweidlem56  37486  stoweidlem59  37489  stoweidlem60  37490  fourier2  37659  2rmoswap  37996  opeliun2xp  38874
  Copyright terms: Public domain W3C validator