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

Definition df-rex 2514
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 2510 . 2  wff  E. x  e.  A  ph
52cv 1618 . . . . 5  class  x
65, 3wcel 1621 . . . 4  wff  x  e.  A
76, 1wa 360 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wex 1537 . 2  wff  E. x
( x  e.  A  /\  ph )
94, 8wb 178 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  2517  rexnal  2518  rexbida  2522  rexbidv2  2530  rexbii2  2536  r2exf  2541  risset  2552  nfre1  2561  rexex  2564  ra4e  2566  ra42e  2568  reximi2  2611  reximdv2  2614  r19.23t  2619  r19.41  2654  reean  2668  rexeqf  2687  rexv  2741  2gencl  2755  3gencl  2756  rcla4e  2816  ceqsrexv  2838  rexab  2865  rexab2  2869  rexrab2  2870  morex  2886  reurex  2890  reu5  2891  reu2  2892  reu6  2893  reu3  2894  2reuswap  2902  rexun  3263  reuss2  3355  reuun2  3358  reupick  3359  reupick3  3360  reximdva0  3373  rabn0  3381  r19.2z  3449  r19.2zb  3450  rexsns  3575  dfuni2  3729  eluni2  3731  elunirab  3740  iuncom4  3810  iunxiun  3882  intexrab  4068  reusv5OLD  4435  elxp2  4614  opeliunxp  4647  xpiundi  4650  xpiundir  4651  dmuni  4795  rnmpt  4832  elrnmpt1  4835  elres  4897  dfima2  4921  dfima3  4922  elima2  4925  dfco2a  5079  imaco  5084  dffo4  5528  dffo5  5529  zfrep6  5600  abrexco  5618  opabex3  5621  abexssex  5633  abexex  5634  isomin  5686  frxp  6077  rdglim2  6331  oarec  6446  oeeu  6487  mapsn  6695  mapsnen  6823  pssnn  6966  unblem2  6995  dffi2  7060  marypha2lem4  7075  marypha2  7076  zfregcl  7192  axinf2  7225  zfinf2  7227  rankuni  7419  scott0  7440  cp  7445  bnd2  7447  infpwfien  7573  aceq1  7628  dfac5lem2  7635  dfac5lem3  7636  dfac2  7641  kmlem3  7662  kmlem6  7665  kmlem8  7667  kmlem14  7673  infmap2  7728  ackbij2  7753  cfub  7759  cfval2  7770  cflim3  7772  cfss  7775  cfslb  7776  isf32lem9  7871  zorn2lem6  8012  iundom2g  8046  winalim2  8198  grothprim  8336  genpass  8513  nqpr  8518  1idpr  8533  ltexprlem4  8543  ltexprlem5  8544  reclem2pr  8552  axrrecex  8665  sup2  9590  infm3  9593  nnunb  9840  2rexuz  10150  nnwos  10165  xrsupsslem  10503  xrinfmsslem  10504  maxprmfct  12666  vdwapun  12895  vdwmc  12899  vdwmc2  12900  ram0  12943  imasleval  13317  isssc  13541  drsdirfi  13916  dirge  14194  odcau  14750  ablfac2  15159  lspprat  15740  lidlnz  15812  isbasis2g  16518  tgval2  16526  ntreq0  16646  cmpfi  16967  is1stc2  17000  2ndcsb  17007  2ndcsep  17017  1stcelcls  17019  hausmapdom  17058  isfbas2  17362  fbssint  17365  isfil2  17383  elfg  17398  fgcl  17405  uffix2  17451  alexsubALTlem4  17576  lpbl  17881  bcthlem5  18582  ubthlem1  21279  axhcompl-zf  21408  isch3  21651  shne0i  21857  cnlnssadj  22490  erdszelem10  22902  ptpcon  22935  umgraex  23046  dedekind  23252  coep  23278  coepr  23279  dffr5  23280  dfpo2  23282  dfon2lem8  23314  tfrALTlem  23444  axfelem18  23531  brimg  23650  dfrdg4  23662  tfrqfree  23663  ellines  23949  fates  24120  dstr  24337  domncnt  24448  ranncnt  24449  dfdir2  24457  apnei  24686  gltpntl2  25239  isconcl7a  25271  bosser  25333  neifg  25486  abrexdom  25571  prdstotbnd  25684  n0el  25891  prtlem17  25910  prter2  25915  psgnunilem4  26586  rexbidar  26816  onfrALTlem5  27000  onfrALTlem2  27004  onfrALTlem1  27006  onfrALTlem5VD  27351  onfrALTlem2VD  27355  onfrALTlem1VD  27356  bnj168  27447  bnj956  27497  bnj1098  27504  bnj1143  27511  bnj1146  27512  bnj1185  27515  bnj1196  27516  bnj600  27640  bnj849  27646  bnj906  27651  bnj916  27654  bnj983  27672  bnj984  27673  bnj1083  27697  bnj1176  27724  bnj1186  27726  bnj1189  27728  bnj1228  27730  bnj1253  27736  bnj1398  27753  bnj1463  27774  bnj1312  27777  bnj1514  27782  islshpat  27896  lsat0cv  27912  lshpsmreu  27988  atex  28284  islpln5  28413  islvol5  28457  pmapglb  28648  pmapglb2N  28649  pmapglb2xN  28650  elpaddn0  28678  pmapjat1  28731  polval2N  28784  osumcllem11N  28844  pexmidlem8N  28855  cdlemftr3  29443  dibelval3  30026  dibglbN  30045  dicelval3  30059  dihglbcpreN  30179  dihglb2  30221  dihjatcclem4  30300  mapdordlem2  30516  mapdrvallem2  30524  mapdpglem3  30554  hdmapglem7a  30809
  Copyright terms: Public domain W3C validator