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

Definition df-rex 2720
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 2715 . 2  wff  E. x  e.  A  ph
52cv 1436 . . . . 5  class  x
65, 3wcel 1872 . . . 4  wff  x  e.  A
76, 1wa 370 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wex 1657 . 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  2811  rexex  2821  rspe  2822  rsp2eOLD  2824  nfre1  2825  reximi2  2831  reximd2a  2834  reximdv2  2835  r19.23t  2842  rexbii2  2864  rexbida  2873  rexbidv2  2874  r2exfOLD  2889  risset  2892  r19.41v  2919  r19.41  2920  reean  2934  rexeqf  2961  reu5  2985  rmo5  2988  cbvrexdva2  3001  rexv  3038  2gencl  3054  3gencl  3055  rspce  3120  ceqsrexv  3147  rexab  3176  rexab2  3180  rexrab2  3181  morex  3197  reu2  3201  reu6  3202  reu3  3203  2reuswap  3217  2reu5lem3  3222  2reu5  3223  ssrexf  3467  rexun  3589  reuss2  3696  reuun2  3699  reupick  3700  reupick3  3701  euelss  3703  reximdva0  3716  rabn0  3725  r19.2z  3831  r19.2zb  3832  rexsns  3975  rexsnsOLD  3976  exsnrex  3980  dfuni2  4164  eluni2  4166  elunirab  4174  iuncom4  4250  iunxiun  4328  intexrab  4526  elxp2  4814  opeliunxp  4848  xpiundi  4851  xpiundir  4852  dmuni  5006  rnmpt  5042  elrnmpt1  5045  elres  5102  dfima2  5132  dfima3  5133  elima2  5136  dfco2a  5297  imaco  5302  elsnxp  5340  dffo4  5997  dffo5  5998  abrexco  6108  isomin  6187  zfrep6  6719  opabex3d  6729  opabex3  6730  abexssex  6733  abexex  6734  frxp  6861  dfrecs3  7046  rdglim2  7105  oarec  7218  oeeu  7259  mapsn  7468  mapsnen  7601  pssnn  7743  unblem2  7777  dffi2  7890  marypha2lem4  7905  marypha2  7906  zfregcl  8062  axinf2  8098  zfinf2  8100  rankuni  8286  scott0  8309  cp  8314  bnd2  8316  infpwfien  8444  aceq1  8499  dfac5lem2  8506  dfac5lem3  8507  dfac2  8512  kmlem3  8533  kmlem6  8536  kmlem8  8538  kmlem14  8544  infmap2  8599  ackbij2  8624  cfub  8630  cfval2  8641  cflim3  8643  cfss  8646  cfslb  8647  isf32lem9  8742  zorn2lem6  8882  iundom2g  8916  winalim2  9072  grothprim  9210  genpass  9385  nqpr  9390  1idpr  9405  ltexprlem4  9415  ltexprlem5  9416  reclem2pr  9424  axrrecex  9538  dedekind  9748  sup2  10516  infm3  10519  nnunb  10816  2rexuz  11162  nnwos  11177  xrsupsslem  11543  xrinfmsslem  11544  ishashinf  12574  cshwsexa  12869  wwlktovfo  12977  maxprmfct  14595  ncoprmgcdne1b  14598  vdwapun  14867  vdwmc  14871  vdwmc2  14872  ram0  14923  imasleval  15390  mreexexlem2d  15494  dfiso2  15620  isssc  15668  drsdirfi  16126  dirge  16426  psgnunilem4  17081  odcau  17199  ablfac2  17665  lspprat  18319  lidlnz  18395  isbasis2g  19905  tgval2  19913  ntreq0  20035  neitr  20138  cmpfi  20365  is1stc2  20399  2ndcsb  20406  2ndcsep  20416  1stcelcls  20418  hausmapdom  20457  isfbas2  20792  fbssint  20795  isfil2  20813  elfg  20828  fgcl  20835  uffix2  20881  alexsubALTlem4  21007  lpbl  21460  metustexhalf  21513  metuel2  21522  restmetu  21527  bcthlem5  22238  umgraex  24992  usgraedg4  25056  uvtx01vtx  25162  3v3e3cycl2  25334  wlknwwlknsur  25382  wlkiswwlksur  25389  wwlkextsur  25401  frisusgranb  25667  frgra3vlem2  25671  3vfriswmgralem  25674  frgrancvvdeqlemC  25709  usg2spot2nb  25735  ubthlem1  26454  axhcompl-zf  26593  isch3  26836  shne0i  27043  cnlnssadj  27675  2reuswap2  28066  rexunirn  28069  rmoxfrdOLD  28070  rmoxfrd  28071  abrexdomjm  28084  abrexexd  28086  iunxsngf  28118  1stpreimas  28232  fpwrelmapffslem  28267  ordtconlem1  28682  ddemeas  29011  omssubaddlem  29079  omssubadd  29080  omssubaddlemOLD  29083  omssubaddOLD  29084  eulerpartlemgvv  29161  bnj168  29490  bnj956  29540  bnj1098  29547  bnj1143  29554  bnj1146  29555  bnj1185  29557  bnj1196  29558  bnj600  29682  bnj849  29688  bnj906  29693  bnj916  29696  bnj983  29714  bnj984  29715  bnj1083  29739  bnj1176  29766  bnj1186  29768  bnj1189  29770  bnj1228  29772  bnj1253  29778  bnj1398  29795  bnj1463  29816  bnj1312  29819  bnj1514  29824  erdszelem10  29875  ptpcon  29908  coep  30342  coepr  30343  dffr5  30344  dfpo2  30346  opelco3  30371  dfon2lem8  30387  brimg  30653  dfrecs2  30666  dfrdg4  30667  ellines  30868  neifg  30976  bj-rexvwv  31386  bj-rexcom4  31389  bj-snglc  31474  bj-snglss  31475  bj-finsumval0  31609  rnmptsn  31644  f1omptsnlem  31645  mptsnunlem  31647  topdifinffinlem  31657  isbasisrelowllem1  31665  isbasisrelowllem2  31666  relowlpssretop  31674  poimirlem30  31877  abrexdom  31964  prdstotbnd  32033  n0el  32342  prtlem17  32359  prter2  32364  islshpat  32495  lsat0cv  32511  lshpsmreu  32587  atex  32883  islpln5  33012  islvol5  33056  pmapglb  33247  pmapglb2N  33248  pmapglb2xN  33249  elpaddn0  33277  pmapjat1  33330  polval2N  33383  osumcllem11N  33443  pexmidlem8N  33454  cdlemftr3  34044  dibelval3  34627  dibglbN  34646  dicelval3  34660  dihglbcpreN  34780  dihglb2  34822  dihjatcclem4  34901  mapdordlem2  35117  mapdrvallem2  35125  mapdpglem3  35155  hdmapglem7a  35410  rp-isfinite5  36075  rp-isfinite6  36076  relintabex  36100  elintima  36158  iunrelexpuztr  36224  cotrclrcl  36247  rexbidar  36712  onfrALTlem5  36821  onfrALTlem2  36825  onfrALTlem1  36827  onfrALTlem5VD  37198  onfrALTlem2VD  37202  onfrALTlem1VD  37203  chordthmALT  37246  rspcegf  37260  cncmpmax  37269  rfcnnnub  37273  suprnmpt  37342  founiiun0  37369  disjinfi  37372  ssfiunibd  37424  infrpge  37471  fsumiunss  37538  islpcn  37602  lptre2pt  37603  stoweidlem14  37757  stoweidlem34  37778  stoweidlem35  37779  stoweidlem43  37787  stoweidlem44  37788  stoweidlem50  37794  stoweidlem54  37798  stoweidlem56  37800  stoweidlem59  37803  stoweidlem60  37804  fourier2  37974  sge0rpcpnf  38114  hoidmvval0b  38259  2rmoswap  38419  ssrelrn  38819  upgrex  38960  uvtxa01vtx0  39209  opeliun2xp  39717
  Copyright terms: Public domain W3C validator