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

Definition df-rex 2562
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 2557 . 2  wff  E. x  e.  A  ph
52cv 1631 . . . . 5  class  x
65, 3wcel 1696 . . . 4  wff  x  e.  A
76, 1wa 358 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wex 1531 . 2  wff  E. x
( x  e.  A  /\  ph )
94, 8wb 176 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  2566  rexnal  2567  rexbida  2571  rexbidv2  2579  rexbii2  2585  r2exf  2592  risset  2603  nfre1  2612  rexex  2615  rspe  2617  rsp2e  2619  reximi2  2662  reximdv2  2665  r19.23t  2670  r19.41  2705  reean  2719  rexeqf  2746  reu5  2766  rmo5  2769  cbvrexdva2  2782  rexv  2815  2gencl  2830  3gencl  2831  rspce  2892  ceqsrexv  2914  rexab  2941  rexab2  2945  rexrab2  2946  morex  2962  reu2  2966  reu6  2967  reu3  2968  2reuswap  2980  2reu5lem3  2985  2reu5  2986  rexun  3368  reuss2  3461  reuun2  3464  reupick  3465  reupick3  3466  reximdva0  3479  rabn0  3487  r19.2z  3556  r19.2zb  3557  rexsns  3684  dfuni2  3845  eluni2  3847  elunirab  3856  iuncom4  3928  iunxiun  4000  intexrab  4186  reusv5OLD  4560  elxp2  4723  opeliunxp  4756  xpiundi  4759  xpiundir  4760  dmuni  4904  rnmpt  4941  elrnmpt1  4944  elres  5006  dfima2  5030  dfima3  5031  elima2  5034  dfco2a  5189  imaco  5194  dffo4  5692  dffo5  5693  zfrep6  5764  abrexco  5782  opabex3  5785  abexssex  5797  abexex  5798  isomin  5850  frxp  6241  rdglim2  6461  oarec  6576  oeeu  6617  mapsn  6825  mapsnen  6954  pssnn  7097  unblem2  7126  dffi2  7192  marypha2lem4  7207  marypha2  7208  zfregcl  7324  axinf2  7357  zfinf2  7359  rankuni  7551  scott0  7572  cp  7577  bnd2  7579  infpwfien  7705  aceq1  7760  dfac5lem2  7767  dfac5lem3  7768  dfac2  7773  kmlem3  7794  kmlem6  7797  kmlem8  7799  kmlem14  7805  infmap2  7860  ackbij2  7885  cfub  7891  cfval2  7902  cflim3  7904  cfss  7907  cfslb  7908  isf32lem9  8003  zorn2lem6  8144  iundom2g  8178  winalim2  8334  grothprim  8472  genpass  8649  nqpr  8654  1idpr  8669  ltexprlem4  8679  ltexprlem5  8680  reclem2pr  8688  axrrecex  8801  sup2  9726  infm3  9729  nnunb  9977  2rexuz  10287  nnwos  10302  xrsupsslem  10641  xrinfmsslem  10642  maxprmfct  12808  vdwapun  13037  vdwmc  13041  vdwmc2  13042  ram0  13085  imasleval  13459  mreexexlem2d  13563  isssc  13713  drsdirfi  14088  dirge  14375  odcau  14931  ablfac2  15340  lspprat  15922  lidlnz  15996  isbasis2g  16702  tgval2  16710  ntreq0  16830  cmpfi  17151  is1stc2  17184  2ndcsb  17191  2ndcsep  17201  1stcelcls  17203  hausmapdom  17242  isfbas2  17546  fbssint  17549  isfil2  17567  elfg  17582  fgcl  17589  uffix2  17635  alexsubALTlem4  17760  lpbl  18065  bcthlem5  18766  ubthlem1  21465  axhcompl-zf  21594  isch3  21837  shne0i  22043  cnlnssadj  22676  2reuswap2  23153  rexunirn  23156  rmoxfrdOLD  23162  rmoxfrd  23163  abrexdomjm  23181  abrexexd  23207  ishashinf  23404  erdszelem10  23746  ptpcon  23779  umgraex  23890  dedekind  24097  coep  24179  coepr  24180  dffr5  24181  dfpo2  24183  dfon2lem8  24217  tfrALTlem  24347  brimg  24547  dfrdg4  24560  tfrqfree  24561  ellines  24847  fates  25058  dstr  25274  domncnt  25385  ranncnt  25386  dfdir2  25394  apnei  25623  gltpntl2  26176  isconcl7a  26208  bosser  26270  neifg  26423  abrexdom  26508  prdstotbnd  26621  n0el  26828  prtlem17  26847  prter2  26852  psgnunilem4  27523  rexbidar  27752  ssrexf  27787  rspcegf  27797  cncmpmax  27806  rfcnnnub  27810  stoweidlem14  27866  stoweidlem27  27879  stoweidlem34  27886  stoweidlem35  27887  stoweidlem43  27895  stoweidlem44  27896  stoweidlem50  27902  stoweidlem54  27906  stoweidlem56  27908  stoweidlem57  27909  stoweidlem59  27911  stoweidlem60  27912  2rmoswap  28065  opabex3d  28190  uvtx01vtx  28305  3v3e3cycl2  28410  frgra3vlem2  28425  3vfriswmgralem  28428  onfrALTlem5  28606  onfrALTlem2  28610  onfrALTlem1  28612  onfrALTlem5VD  28977  onfrALTlem2VD  28981  onfrALTlem1VD  28982  chordthmALT  29026  bnj168  29074  bnj956  29124  bnj1098  29131  bnj1143  29138  bnj1146  29139  bnj1185  29142  bnj1196  29143  bnj600  29267  bnj849  29273  bnj906  29278  bnj916  29281  bnj983  29299  bnj984  29300  bnj1083  29324  bnj1176  29351  bnj1186  29353  bnj1189  29355  bnj1228  29357  bnj1253  29363  bnj1398  29380  bnj1463  29401  bnj1312  29404  bnj1514  29409  islshpat  29829  lsat0cv  29845  lshpsmreu  29921  atex  30217  islpln5  30346  islvol5  30390  pmapglb  30581  pmapglb2N  30582  pmapglb2xN  30583  elpaddn0  30611  pmapjat1  30664  polval2N  30717  osumcllem11N  30777  pexmidlem8N  30788  cdlemftr3  31376  dibelval3  31959  dibglbN  31978  dicelval3  31992  dihglbcpreN  32112  dihglb2  32154  dihjatcclem4  32233  mapdordlem2  32449  mapdrvallem2  32457  mapdpglem3  32487  hdmapglem7a  32742
  Copyright terms: Public domain W3C validator