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

Definition df-rex 2754
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 2749 . 2  wff  E. x  e.  A  ph
52cv 1453 . . . . 5  class  x
65, 3wcel 1897 . . . 4  wff  x  e.  A
76, 1wa 375 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wex 1673 . 2  wff  E. x
( x  e.  A  /\  ph )
94, 8wb 189 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  2845  rexex  2855  rspe  2856  rsp2eOLD  2858  nfre1  2859  reximi2  2865  reximd2a  2868  reximdv2  2869  r19.23t  2876  rexbii2  2898  rexbida  2907  rexbidv2  2908  r2exfOLD  2923  risset  2926  r19.41v  2953  r19.41  2954  reean  2968  rexeqf  2995  reu5  3019  rmo5  3022  cbvrexdva2  3035  rexv  3073  2gencl  3089  3gencl  3090  rspce  3156  ceqsrexv  3183  rexab  3212  rexab2  3216  rexrab2  3217  morex  3233  reu2  3237  reu6  3238  reu3  3239  2reuswap  3253  2reu5lem3  3258  2reu5  3259  ssrexf  3503  rexun  3625  reuss2  3734  reuun2  3737  reupick  3738  reupick3  3739  euelss  3741  reximdva0  3754  rabn0  3763  r19.2z  3869  r19.2zb  3870  rexsns  4015  rexsnsOLD  4016  exsnrex  4020  dfuni2  4213  eluni2  4215  elunirab  4223  iuncom4  4299  iunxiun  4377  intexrab  4575  elxp2  4870  opeliunxp  4904  xpiundi  4907  xpiundir  4908  dmuni  5062  rnmpt  5098  elrnmpt1  5101  elres  5158  dfima2  5188  dfima3  5189  elima2  5192  dfco2a  5353  imaco  5358  elsnxp  5396  dffo4  6060  dffo5  6061  abrexco  6173  isomin  6252  zfrep6  6787  opabex3d  6797  opabex3  6798  abexssex  6801  abexex  6802  frxp  6932  dfrecs3  7116  rdglim2  7175  oarec  7288  oeeu  7329  mapsn  7538  mapsnen  7672  pssnn  7815  unblem2  7849  dffi2  7962  marypha2lem4  7977  marypha2  7978  zfregcl  8134  axinf2  8170  zfinf2  8172  rankuni  8359  scott0  8382  cp  8387  bnd2  8389  infpwfien  8518  aceq1  8573  dfac5lem2  8580  dfac5lem3  8581  dfac2  8586  kmlem3  8607  kmlem6  8610  kmlem8  8612  kmlem14  8618  infmap2  8673  ackbij2  8698  cfub  8704  cfval2  8715  cflim3  8717  cfss  8720  cfslb  8721  isf32lem9  8816  zorn2lem6  8956  iundom2g  8990  winalim2  9146  grothprim  9284  genpass  9459  nqpr  9464  1idpr  9479  ltexprlem4  9489  ltexprlem5  9490  reclem2pr  9498  axrrecex  9612  dedekind  9822  sup2  10592  infm3  10595  nnunb  10893  2rexuz  11239  nnwos  11254  xrsupsslem  11620  xrinfmsslem  11621  ishashinf  12658  cshwsexa  12959  wwlktovfo  13081  maxprmfct  14700  ncoprmgcdne1b  14703  vdwapun  14972  vdwmc  14976  vdwmc2  14977  ram0  15028  imasleval  15495  mreexexlem2d  15599  dfiso2  15725  isssc  15773  drsdirfi  16231  dirge  16531  psgnunilem4  17186  odcau  17304  ablfac2  17770  lspprat  18424  lidlnz  18500  isbasis2g  20011  tgval2  20019  ntreq0  20141  neitr  20244  cmpfi  20471  is1stc2  20505  2ndcsb  20512  2ndcsep  20522  1stcelcls  20524  hausmapdom  20563  isfbas2  20898  fbssint  20901  isfil2  20919  elfg  20934  fgcl  20941  uffix2  20987  alexsubALTlem4  21113  lpbl  21566  metustexhalf  21619  metuel2  21628  restmetu  21633  bcthlem5  22344  umgraex  25098  usgraedg4  25162  uvtx01vtx  25268  3v3e3cycl2  25440  wlknwwlknsur  25488  wlkiswwlksur  25495  wwlkextsur  25507  frisusgranb  25773  frgra3vlem2  25777  3vfriswmgralem  25780  frgrancvvdeqlemC  25815  usg2spot2nb  25841  ubthlem1  26560  axhcompl-zf  26699  isch3  26942  shne0i  27149  cnlnssadj  27781  2reuswap2  28172  rexunirn  28175  rmoxfrdOLD  28176  rmoxfrd  28177  abrexdomjm  28189  abrexexd  28191  iunxsngf  28220  1stpreimas  28334  fpwrelmapffslem  28365  ordtconlem1  28778  ddemeas  29107  omssubaddlem  29175  omssubadd  29176  omssubaddlemOLD  29179  omssubaddOLD  29180  eulerpartlemgvv  29257  bnj168  29586  bnj956  29636  bnj1098  29643  bnj1143  29650  bnj1146  29651  bnj1185  29653  bnj1196  29654  bnj600  29778  bnj849  29784  bnj906  29789  bnj916  29792  bnj983  29810  bnj984  29811  bnj1083  29835  bnj1176  29862  bnj1186  29864  bnj1189  29866  bnj1228  29868  bnj1253  29874  bnj1398  29891  bnj1463  29912  bnj1312  29915  bnj1514  29920  erdszelem10  29971  ptpcon  30004  coep  30439  coepr  30440  dffr5  30441  dfpo2  30443  opelco3  30468  dfon2lem8  30484  brimg  30752  dfrecs2  30765  dfrdg4  30766  ellines  30967  neifg  31075  bj-rexvwv  31519  bj-rexcom4  31522  bj-snglc  31607  bj-snglss  31608  bj-dfmpt2a  31674  bj-finsumval0  31746  rnmptsn  31781  f1omptsnlem  31782  mptsnunlem  31784  topdifinffinlem  31794  isbasisrelowllem1  31802  isbasisrelowllem2  31803  relowlpssretop  31811  poimirlem30  32014  abrexdom  32101  prdstotbnd  32170  n0el  32477  prtlem17  32492  prter2  32497  islshpat  32627  lsat0cv  32643  lshpsmreu  32719  atex  33015  islpln5  33144  islvol5  33188  pmapglb  33379  pmapglb2N  33380  pmapglb2xN  33381  elpaddn0  33409  pmapjat1  33462  polval2N  33515  osumcllem11N  33575  pexmidlem8N  33586  cdlemftr3  34176  dibelval3  34759  dibglbN  34778  dicelval3  34792  dihglbcpreN  34912  dihglb2  34954  dihjatcclem4  35033  mapdordlem2  35249  mapdrvallem2  35257  mapdpglem3  35287  hdmapglem7a  35542  rp-isfinite5  36206  rp-isfinite6  36207  relintabex  36231  elintima  36289  iunrelexpuztr  36355  cotrclrcl  36378  rexbidar  36842  onfrALTlem5  36951  onfrALTlem2  36955  onfrALTlem1  36957  onfrALTlem5VD  37321  onfrALTlem2VD  37325  onfrALTlem1VD  37326  chordthmALT  37369  rspcegf  37383  cncmpmax  37392  rfcnnnub  37396  rspcef  37453  inn0f  37454  suprnmpt  37476  founiiun0  37502  disjinfi  37505  mapsnd  37513  mapsnend  37517  ssfiunibd  37564  infrpge  37611  fsumiunss  37691  islpcn  37756  lptre2pt  37757  stoweidlem14  37911  stoweidlem34  37932  stoweidlem35  37933  stoweidlem43  37941  stoweidlem44  37942  stoweidlem50  37948  stoweidlem54  37952  stoweidlem56  37954  stoweidlem59  37957  stoweidlem60  37958  fourier2  38128  qndenserrnbllem  38200  qndenserrn  38205  sge0rpcpnf  38300  hoidmvval0b  38449  hoiqssbllem3  38483  2rmoswap  38642  n0rex  39027  ssrelrn  39051  upgrex  39230  uvtxa01vtx0  39518  uhgrvd00  39620  opeliun2xp  40386
  Copyright terms: Public domain W3C validator