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

Definition df-rex 2655
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  set  x
3 cA . . 3  class  A
41, 2, 3wrex 2650 . 2  wff  E. x  e.  A  ph
52cv 1648 . . . . 5  class  x
65, 3wcel 1717 . . . 4  wff  x  e.  A
76, 1wa 359 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wex 1547 . 2  wff  E. x
( x  e.  A  /\  ph )
94, 8wb 177 1  wff  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
Colors of variables: wff set class
This definition is referenced by:  ralnex  2659  rexnal  2660  rexbida  2664  rexbidv2  2672  rexbii2  2678  r2exf  2685  risset  2696  nfre1  2705  rexex  2708  rspe  2710  rsp2e  2712  reximi2  2755  reximdv2  2758  r19.23t  2763  r19.41  2803  reean  2817  rexeqf  2844  reu5  2864  rmo5  2867  cbvrexdva2  2880  rexv  2913  2gencl  2928  3gencl  2929  rspce  2990  ceqsrexv  3012  rexab  3040  rexab2  3044  rexrab2  3045  morex  3061  reu2  3065  reu6  3066  reu3  3067  2reuswap  3079  2reu5lem3  3084  2reu5  3085  rexun  3470  reuss2  3564  reuun2  3567  reupick  3568  reupick3  3569  reximdva0  3582  rabn0  3590  r19.2z  3660  r19.2zb  3661  rexsns  3788  exsnrex  3791  dfuni2  3959  eluni2  3961  elunirab  3970  iuncom4  4042  iunxiun  4114  intexrab  4300  reusv5OLD  4673  elxp2  4836  opeliunxp  4869  xpiundi  4872  xpiundir  4873  dmuni  5019  rnmpt  5056  elrnmpt1  5059  elres  5121  dfima2  5145  dfima3  5146  elima2  5149  dfco2a  5310  imaco  5315  dffo4  5824  dffo5  5825  zfrep6  5907  abrexco  5925  opabex3d  5928  opabex3  5929  abexssex  5941  abexex  5942  isomin  5996  frxp  6392  rdglim2  6626  oarec  6741  oeeu  6782  mapsn  6991  mapsnen  7120  pssnn  7263  unblem2  7296  dffi2  7363  marypha2lem4  7378  marypha2  7379  zfregcl  7495  axinf2  7528  zfinf2  7530  rankuni  7722  scott0  7743  cp  7748  bnd2  7750  infpwfien  7876  aceq1  7931  dfac5lem2  7938  dfac5lem3  7939  dfac2  7944  kmlem3  7965  kmlem6  7968  kmlem8  7970  kmlem14  7976  infmap2  8031  ackbij2  8056  cfub  8062  cfval2  8073  cflim3  8075  cfss  8078  cfslb  8079  isf32lem9  8174  zorn2lem6  8314  iundom2g  8348  winalim2  8504  grothprim  8642  genpass  8819  nqpr  8824  1idpr  8839  ltexprlem4  8849  ltexprlem5  8850  reclem2pr  8858  axrrecex  8971  sup2  9896  infm3  9899  nnunb  10149  2rexuz  10461  nnwos  10476  xrsupsslem  10817  xrinfmsslem  10818  maxprmfct  13040  vdwapun  13269  vdwmc  13273  vdwmc2  13274  ram0  13317  imasleval  13693  mreexexlem2d  13797  isssc  13947  drsdirfi  14322  dirge  14609  odcau  15165  ablfac2  15574  lspprat  16152  lidlnz  16226  isbasis2g  16936  tgval2  16944  ntreq0  17064  neitr  17166  cmpfi  17393  is1stc2  17426  2ndcsb  17433  2ndcsep  17443  1stcelcls  17445  hausmapdom  17484  isfbas2  17788  fbssint  17791  isfil2  17809  elfg  17824  fgcl  17831  uffix2  17877  alexsubALTlem4  18002  lpbl  18423  metustexhalf  18476  metuel2  18485  restmetu  18489  bcthlem5  19150  umgraex  21225  usgraedg4  21272  uvtx01vtx  21367  3v3e3cycl2  21499  ubthlem1  22220  axhcompl-zf  22349  isch3  22592  shne0i  22798  cnlnssadj  23431  2reuswap2  23819  rexunirn  23822  rmoxfrdOLD  23823  rmoxfrd  23824  abrexdomjm  23832  abrexexd  23834  ishashinf  23997  erdszelem10  24665  ptpcon  24699  dedekind  24966  coep  25132  coepr  25133  dffr5  25134  dfpo2  25136  dfon2lem8  25170  tfrALTlem  25300  brimg  25500  dfrdg4  25513  tfrqfree  25514  ellines  25800  neifg  26091  abrexdom  26123  prdstotbnd  26194  n0el  26399  prtlem17  26416  prter2  26421  psgnunilem4  27089  rexbidar  27317  ssrexf  27352  rspcegf  27362  cncmpmax  27371  rfcnnnub  27375  stoweidlem14  27431  stoweidlem27  27444  stoweidlem34  27451  stoweidlem35  27452  stoweidlem43  27460  stoweidlem44  27461  stoweidlem50  27467  stoweidlem54  27471  stoweidlem56  27473  stoweidlem59  27476  stoweidlem60  27477  2rmoswap  27630  frisusgranb  27750  frgra3vlem2  27754  3vfriswmgralem  27757  frgrancvvdeqlemC  27791  onfrALTlem5  27971  onfrALTlem2  27975  onfrALTlem1  27977  onfrALTlem5VD  28338  onfrALTlem2VD  28342  onfrALTlem1VD  28343  chordthmALT  28387  bnj168  28435  bnj956  28485  bnj1098  28492  bnj1143  28499  bnj1146  28500  bnj1185  28503  bnj1196  28504  bnj600  28628  bnj849  28634  bnj906  28639  bnj916  28642  bnj983  28660  bnj984  28661  bnj1083  28685  bnj1176  28712  bnj1186  28714  bnj1189  28716  bnj1228  28718  bnj1253  28724  bnj1398  28741  bnj1463  28762  bnj1312  28765  bnj1514  28770  islshpat  29132  lsat0cv  29148  lshpsmreu  29224  atex  29520  islpln5  29649  islvol5  29693  pmapglb  29884  pmapglb2N  29885  pmapglb2xN  29886  elpaddn0  29914  pmapjat1  29967  polval2N  30020  osumcllem11N  30080  pexmidlem8N  30091  cdlemftr3  30679  dibelval3  31262  dibglbN  31281  dicelval3  31295  dihglbcpreN  31415  dihglb2  31457  dihjatcclem4  31536  mapdordlem2  31752  mapdrvallem2  31760  mapdpglem3  31790  hdmapglem7a  32045
  Copyright terms: Public domain W3C validator