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

Definition df-rex 2672
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 2667 . 2  wff  E. x  e.  A  ph
52cv 1648 . . . . 5  class  x
65, 3wcel 1721 . . . 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  2676  rexnal  2677  rexbida  2681  rexbidv2  2689  rexbii2  2695  r2exf  2702  risset  2713  nfre1  2722  rexex  2725  rspe  2727  rsp2e  2729  reximi2  2772  reximdv2  2775  r19.23t  2780  r19.41  2820  reean  2834  rexeqf  2861  reu5  2881  rmo5  2884  cbvrexdva2  2897  rexv  2930  2gencl  2945  3gencl  2946  rspce  3007  ceqsrexv  3029  rexab  3057  rexab2  3061  rexrab2  3062  morex  3078  reu2  3082  reu6  3083  reu3  3084  2reuswap  3096  2reu5lem3  3101  2reu5  3102  rexun  3487  reuss2  3581  reuun2  3584  reupick  3585  reupick3  3586  reximdva0  3599  rabn0  3607  r19.2z  3677  r19.2zb  3678  rexsns  3805  exsnrex  3808  dfuni2  3977  eluni2  3979  elunirab  3988  iuncom4  4060  iunxiun  4133  intexrab  4319  reusv5OLD  4692  elxp2  4855  opeliunxp  4888  xpiundi  4891  xpiundir  4892  dmuni  5038  rnmpt  5075  elrnmpt1  5078  elres  5140  dfima2  5164  dfima3  5165  elima2  5168  dfco2a  5329  imaco  5334  dffo4  5844  dffo5  5845  zfrep6  5927  abrexco  5945  opabex3d  5948  opabex3  5949  abexssex  5961  abexex  5962  isomin  6016  frxp  6415  rdglim2  6649  oarec  6764  oeeu  6805  mapsn  7014  mapsnen  7143  pssnn  7286  unblem2  7319  dffi2  7386  marypha2lem4  7401  marypha2  7402  zfregcl  7518  axinf2  7551  zfinf2  7553  rankuni  7745  scott0  7766  cp  7771  bnd2  7773  infpwfien  7899  aceq1  7954  dfac5lem2  7961  dfac5lem3  7962  dfac2  7967  kmlem3  7988  kmlem6  7991  kmlem8  7993  kmlem14  7999  infmap2  8054  ackbij2  8079  cfub  8085  cfval2  8096  cflim3  8098  cfss  8101  cfslb  8102  isf32lem9  8197  zorn2lem6  8337  iundom2g  8371  winalim2  8527  grothprim  8665  genpass  8842  nqpr  8847  1idpr  8862  ltexprlem4  8872  ltexprlem5  8873  reclem2pr  8881  axrrecex  8994  sup2  9920  infm3  9923  nnunb  10173  2rexuz  10485  nnwos  10500  xrsupsslem  10841  xrinfmsslem  10842  maxprmfct  13068  vdwapun  13297  vdwmc  13301  vdwmc2  13302  ram0  13345  imasleval  13721  mreexexlem2d  13825  isssc  13975  drsdirfi  14350  dirge  14637  odcau  15193  ablfac2  15602  lspprat  16180  lidlnz  16254  isbasis2g  16968  tgval2  16976  ntreq0  17096  neitr  17198  cmpfi  17425  is1stc2  17458  2ndcsb  17465  2ndcsep  17475  1stcelcls  17477  hausmapdom  17516  isfbas2  17820  fbssint  17823  isfil2  17841  elfg  17856  fgcl  17863  uffix2  17909  alexsubALTlem4  18034  lpbl  18486  metustexhalfOLD  18546  metustexhalf  18547  metuel2  18562  restmetu  18570  bcthlem5  19234  umgraex  21311  usgraedg4  21359  uvtx01vtx  21454  3v3e3cycl2  21604  ubthlem1  22325  axhcompl-zf  22454  isch3  22697  shne0i  22903  cnlnssadj  23536  2reuswap2  23928  rexunirn  23931  rmoxfrdOLD  23932  rmoxfrd  23933  abrexdomjm  23941  abrexexd  23943  ishashinf  24112  erdszelem10  24839  ptpcon  24873  dedekind  25140  coep  25322  coepr  25323  dffr5  25324  dfpo2  25326  dfon2lem8  25360  tfrALTlem  25490  brimg  25690  dfrdg4  25703  tfrqfree  25704  ellines  25990  neifg  26290  abrexdom  26322  prdstotbnd  26393  n0el  26598  prtlem17  26615  prter2  26620  psgnunilem4  27288  rexbidar  27516  ssrexf  27551  rspcegf  27561  cncmpmax  27570  rfcnnnub  27574  stoweidlem14  27630  stoweidlem27  27643  stoweidlem34  27650  stoweidlem35  27651  stoweidlem43  27659  stoweidlem44  27660  stoweidlem50  27666  stoweidlem54  27670  stoweidlem56  27672  stoweidlem59  27675  stoweidlem60  27676  2rmoswap  27829  frisusgranb  28101  frgra3vlem2  28105  3vfriswmgralem  28108  frgrancvvdeqlemC  28142  usg2spot2nb  28168  onfrALTlem5  28339  onfrALTlem2  28343  onfrALTlem1  28345  onfrALTlem5VD  28706  onfrALTlem2VD  28710  onfrALTlem1VD  28711  chordthmALT  28755  bnj168  28803  bnj956  28853  bnj1098  28860  bnj1143  28867  bnj1146  28868  bnj1185  28871  bnj1196  28872  bnj600  28996  bnj849  29002  bnj906  29007  bnj916  29010  bnj983  29028  bnj984  29029  bnj1083  29053  bnj1176  29080  bnj1186  29082  bnj1189  29084  bnj1228  29086  bnj1253  29092  bnj1398  29109  bnj1463  29130  bnj1312  29133  bnj1514  29138  islshpat  29500  lsat0cv  29516  lshpsmreu  29592  atex  29888  islpln5  30017  islvol5  30061  pmapglb  30252  pmapglb2N  30253  pmapglb2xN  30254  elpaddn0  30282  pmapjat1  30335  polval2N  30388  osumcllem11N  30448  pexmidlem8N  30459  cdlemftr3  31047  dibelval3  31630  dibglbN  31649  dicelval3  31663  dihglbcpreN  31783  dihglb2  31825  dihjatcclem4  31904  mapdordlem2  32120  mapdrvallem2  32128  mapdpglem3  32158  hdmapglem7a  32413
  Copyright terms: Public domain W3C validator