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

Definition df-rex 2901
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 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))

Detailed syntax breakdown of Definition df-rex
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
3 cA . . 3 class 𝐴
41, 2, 3wrex 2896 . 2 wff 𝑥𝐴 𝜑
52cv 1473 . . . . 5 class 𝑥
65, 3wcel 1976 . . . 4 wff 𝑥𝐴
76, 1wa 382 . . 3 wff (𝑥𝐴𝜑)
87, 2wex 1694 . 2 wff 𝑥(𝑥𝐴𝜑)
94, 8wb 194 1 wff (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  ralnex  2974  ralnexOLD  2975  rexex  2984  rspe  2985  nfre1  2987  reximi2  2992  reximd2a  2995  reximdv2  2996  r19.23t  3002  rexbii2  3020  rexbida  3028  rexbidv2  3029  risset  3043  r19.41v  3069  r19.41  3070  reean  3084  rexeqf  3111  reu5  3135  rmo5  3138  cbvrexdva2  3151  rexv  3192  2gencl  3208  3gencl  3209  rspce  3276  ceqsrexv  3305  rexab  3335  rexab2  3339  rexrab2  3340  morex  3356  reu2  3360  reu6  3361  reu3  3362  2reuswap  3376  2reu5lem3  3381  2reu5  3382  ssrexf  3627  rexun  3754  reuss2  3865  reuun2  3868  reupick  3869  reupick3  3870  euelss  3872  reximdva0  3890  rabn0OLD  3912  r19.2z  4011  r19.2zb  4012  rexsns  4163  exsnrex  4167  dfuni2  4368  eluni2  4370  elunirab  4378  iuncom4  4458  iunxiun  4538  intexrab  4744  elxp2OLD  5046  opeliunxp  5082  xpiundi  5085  xpiundir  5086  dmuni  5242  rnmpt  5278  elrnmpt1  5281  elres  5341  dfima2  5373  dfima3  5374  elima2  5377  dfco2a  5537  imaco  5542  elsnxp  5579  elsnxpOLD  5580  dffo4  6267  dffo5  6268  abrexco  6383  isomin  6464  zfrep6  7004  opabex3d  7014  opabex3  7015  abexssex  7018  abexex  7019  frxp  7151  dfrecs3  7333  rdglim2  7392  oarec  7506  oeeu  7547  mapsn  7762  mapsnen  7897  pssnn  8040  unblem2  8075  dffi2  8189  marypha2lem4  8204  marypha2  8205  zfregcl  8359  zfregclOLD  8361  axinf2  8397  zfinf2  8399  rankuni  8586  scott0  8609  cp  8614  bnd2  8616  infpwfien  8745  aceq1  8800  dfac5lem2  8807  dfac5lem3  8808  dfac2  8813  kmlem3  8834  kmlem6  8837  kmlem8  8839  kmlem14  8845  infmap2  8900  ackbij2  8925  cfub  8931  cfval2  8942  cflim3  8944  cfss  8947  cfslb  8948  isf32lem9  9043  zorn2lem6  9183  iundom2g  9218  winalim2  9374  grothprim  9512  genpass  9687  nqpr  9692  1idpr  9707  ltexprlem4  9717  ltexprlem5  9718  reclem2pr  9726  axrrecex  9840  dedekind  10051  sup2  10830  infm3  10833  nnunb  11137  2rexuz  11574  nnwos  11589  xrsupsslem  11967  xrinfmsslem  11968  ishashinf  13058  cshwsexa  13369  wwlktovfo  13497  ncoprmgcdne1b  15149  maxprmfct  15207  vdwapun  15464  vdwmc  15468  vdwmc2  15469  ram0  15512  imasleval  15972  mreexexlem2d  16076  dfiso2  16203  isssc  16251  drsdirfi  16709  dirge  17008  psgnunilem4  17688  odcau  17790  ablfac2  18259  lspprat  18922  lidlnz  18997  isbasis2g  20510  tgval2  20518  ntreq0  20638  neitr  20741  cmpfi  20968  is1stc2  21002  2ndcsb  21009  2ndcsep  21019  1stcelcls  21021  hausmapdom  21060  isfbas2  21396  fbssint  21399  isfil2  21417  elfg  21432  fgcl  21439  uffix2  21485  alexsubALTlem4  21611  lpbl  22065  metustexhalf  22118  metuel2  22127  restmetu  22132  bcthlem5  22877  umgraex  25645  usgraedg4  25709  uvtx01vtx  25813  3v3e3cycl2  25985  wlknwwlknsur  26033  wlkiswwlksur  26040  wwlkextsur  26052  frisusgranb  26317  frgra3vlem2  26321  3vfriswmgralem  26324  frgrancvvdeqlemC  26359  usg2spot2nb  26385  ubthlem1  26903  axhcompl-zf  27032  isch3  27275  shne0i  27484  cnlnssadj  28116  2reuswap2  28505  rexunirn  28508  rmoxfrdOLD  28509  rmoxfrd  28510  abrexdomjm  28522  abrexexd  28524  iunxsngf  28551  1stpreimas  28659  fpwrelmapffslem  28688  ordtconlem1  29091  ddemeas  29419  omssubaddlem  29481  omssubadd  29482  eulerpartlemgvv  29558  bnj168  29845  bnj956  29894  bnj1098  29901  bnj1143  29908  bnj1146  29909  bnj1185  29911  bnj1196  29912  bnj600  30036  bnj849  30042  bnj906  30047  bnj916  30050  bnj983  30068  bnj984  30069  bnj1083  30093  bnj1176  30120  bnj1186  30122  bnj1189  30124  bnj1228  30126  bnj1253  30132  bnj1398  30149  bnj1463  30170  bnj1312  30173  bnj1514  30178  erdszelem10  30229  ptpcon  30262  coep  30687  coepr  30688  dffr5  30689  dfpo2  30691  opelco3  30716  dfon2lem8  30732  brimg  31007  dfrecs2  31020  dfrdg4  31021  ellines  31222  neifg  31329  bj-rexvwv  31843  bj-rexcom4  31846  bj-snglc  31933  bj-snglss  31934  bj-rest10  32005  bj-restn0  32007  bj-restpw  32009  bj-rest0  32010  bj-restb  32011  bj-restuni  32014  bj-dfmpt2a  32035  bj-finsumval0  32107  rnmptsn  32141  f1omptsnlem  32142  mptsnunlem  32144  topdifinffinlem  32154  isbasisrelowllem1  32162  isbasisrelowllem2  32163  relowlpssretop  32171  poimirlem30  32392  abrexdom  32478  prdstotbnd  32546  n0el  32947  prtlem17  32962  prter2  32967  islshpat  33105  lsat0cv  33121  lshpsmreu  33197  atex  33493  islpln5  33622  islvol5  33666  pmapglb  33857  pmapglb2N  33858  pmapglb2xN  33859  elpaddn0  33887  pmapjat1  33940  polval2N  33993  osumcllem11N  34053  pexmidlem8N  34064  cdlemftr3  34654  dibelval3  35237  dibglbN  35256  dicelval3  35270  dihglbcpreN  35390  dihglb2  35432  dihjatcclem4  35511  mapdordlem2  35727  mapdrvallem2  35735  mapdpglem3  35765  hdmapglem7a  36020  rp-isfinite5  36665  rp-isfinite6  36666  relintabex  36689  elintima  36747  iunrelexpuztr  36813  cotrclrcl  36836  neik0pk1imk0  37148  ntrneineine0lem  37184  ntrneineine1lem  37185  ntrneiel2  37187  rexbidar  37454  onfrALTlem5  37561  onfrALTlem2  37565  onfrALTlem1  37567  onfrALTlem5VD  37926  onfrALTlem2VD  37930  onfrALTlem1VD  37931  chordthmALT  37974  rspcegf  37988  cncmpmax  37997  rfcnnnub  38001  rspcef  38050  inn0f  38051  nssrex  38070  eluni2f  38098  eliin2f  38099  suprnmpt  38133  founiiun0  38155  disjinfi  38158  mapsnd  38166  mapsnend  38169  ssfiunibd  38247  infrpge  38291  fsumiunss  38425  islpcn  38489  lptre2pt  38490  stoweidlem14  38690  stoweidlem34  38710  stoweidlem35  38711  stoweidlem43  38719  stoweidlem44  38720  stoweidlem50  38726  stoweidlem54  38730  stoweidlem56  38732  stoweidlem59  38735  stoweidlem60  38736  fourier2  38903  qndenserrnbllem  38973  qndenserrn  38978  sge0rpcpnf  39097  hoidmvval0b  39263  hoiqssbllem3  39297  2rmoswap  39616  n0rex  40094  ssrelrn  40115  upgrex  40299  uvtxa01vtx0  40604  uhgrvd00  40731  1wlkpwwlkf1ouspgr  41057  wlknwwlksnsur  41068  wlkwwlksur  41075  wwlksnextsur  41087  frcond3  41421  frgr3vlem2  41425  3vfriswmgrlem  41428  frgrncvvdeqlemC  41459  fusgr2wsp2nb  41479  opeliun2xp  41885
  Copyright terms: Public domain W3C validator