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 3144
Description: Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22.

Note: This notation is most often used to express that 𝜑 holds for at least one element of a given class 𝐴. For this reading 𝑥𝐴 is required, though, for example, asserted when 𝑥 and 𝐴 are disjoint.

Should instead 𝐴 depend on 𝑥, you rather assert at least one 𝑥 fulfilling 𝜑 happens to be contained in the corresponding 𝐴(𝑥). This interpretation is rarely needed (see also df-ral 3143). (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 3139 . 2 wff 𝑥𝐴 𝜑
52cv 1527 . . . . 5 class 𝑥
65, 3wcel 2105 . . . 4 wff 𝑥𝐴
76, 1wa 396 . . 3 wff (𝑥𝐴𝜑)
87, 2wex 1771 . 2 wff 𝑥(𝑥𝐴𝜑)
94, 8wb 207 1 wff (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  ralnex  3236  rexex  3240  reximi2  3244  rexbii2  3245  rexcom4  3249  rexanidOLD  3253  risset  3267  reximdv2  3271  rexbidv2  3295  rspe  3304  nfre1  3306  reximd2a  3312  r19.23t  3313  rexbida  3318  ralrexbid  3322  r19.12  3324  r19.41v  3347  r19.41  3348  rexcom  3355  reeanlem  3366  rexeqf  3399  reu5  3431  rmo5  3435  cbvrexvw  3451  cbvrexdva2  3458  cbvrexdva2OLD  3459  rexv  3521  2gencl  3536  3gencl  3537  rspce  3611  ceqsrexv  3648  rexab  3685  rexab2  3690  rexab2OLD  3691  rexrab2  3692  morex  3709  reu2  3715  reu6  3716  reu3  3717  2reuswap  3736  2reuswap2  3737  2reu5lem3  3747  2reu5  3748  2rmoswap  3751  ssrexf  4030  rexdifi  4121  rexun  4165  reuss2  4282  reuun2  4285  reupick  4286  reupick3  4287  euelss  4289  reximdva0  4311  n0rex  4313  n0el  4320  r19.2z  4438  r19.2zb  4439  rexsns  4601  exsnrex  4612  dfuni2  4834  eluni2  4836  elunirab  4844  iuncom4  4920  iunxiun  5011  axrep6  5189  axsepgfromrep  5193  intexrab  5235  opeliunxp  5613  xpiundi  5616  xpiundir  5617  ssrelrn  5757  dmuni  5777  rnmpt  5821  elrnmpt1  5824  dfima2  5925  dfima3  5926  elima2  5929  dfco2a  6093  imaco  6098  elsnxp  6136  dffo4  6862  dffo5  6863  abrexco  6994  isomin  7079  zfrep6  7647  opabex3d  7657  opabex3rd  7658  opabex3  7659  abexssex  7662  abexex  7663  frxp  7811  dfrecs3  8000  rdglim2  8059  oarec  8178  oeeu  8219  mapsnd  8439  mapsnend  8577  pssnn  8725  unblem2  8760  dffi2  8876  marypha2lem4  8891  marypha2  8892  zfregcl  9047  axinf2  9092  zfinf2  9094  rankuni  9281  scott0  9304  cp  9309  bnd2  9311  infpwfien  9477  aceq1  9532  dfac5lem2  9539  dfac5lem3  9540  dfac2b  9545  kmlem3  9567  kmlem6  9570  kmlem8  9572  kmlem14  9578  infmap2  9629  ackbij2  9654  cfub  9660  cfval2  9671  cflim3  9673  cfss  9676  cfslb  9677  isf32lem9  9772  zorn2lem6  9912  iundom2g  9951  winalim2  10107  grothprim  10245  genpass  10420  nqpr  10425  1idpr  10440  ltexprlem4  10450  ltexprlem5  10451  reclem2pr  10459  axrrecex  10574  dedekind  10792  sup2  11586  infm3  11589  nnunb  11882  2rexuz  12289  nnwos  12304  xrsupsslem  12690  xrinfmsslem  12691  hashgt23el  13775  ishashinf  13811  cshwsexa  14176  wwlktovfo  14312  maxprmfct  16043  vdwapun  16300  vdwmc  16304  vdwmc2  16305  ram0  16348  imasleval  16804  mreexexlem2d  16906  dfiso2  17032  isssc  17080  drsdirfi  17538  dirge  17837  pwmnd  18042  psgnunilem4  18556  odcau  18660  ablfac2  19142  lspprat  19856  lidlnz  19931  isbasis2g  21486  tgval2  21494  ntreq0  21615  neitr  21718  cmpfi  21946  is1stc2  21980  2ndcsb  21987  2ndcsep  21997  1stcelcls  21999  hausmapdom  22038  isfbas2  22373  fbssint  22376  isfil2  22394  elfg  22409  fgcl  22416  uffix2  22462  alexsubALTlem4  22588  lpbl  23042  metustexhalf  23095  metuel2  23104  restmetu  23109  bcthlem5  23860  upgrex  26805  uvtx01vtx  27107  uhgrvd00  27244  wlkswwlksf1o  27585  wwlksnextsurj  27606  frcond3  27976  frgr3vlem2  27981  3vfriswmgrlem  27984  frgrncvvdeqlem9  28014  ubthlem1  28575  axhcompl-zf  28703  isch3  28946  shne0i  29153  cnlnssadj  29785  reuxfrdf  30183  rexunirn  30184  rmoxfrd  30185  dmrab  30188  abrexdomjm  30195  abrexexd  30197  iunrnmptss  30246  1stpreimas  30368  fpwrelmapffslem  30395  qsxpid  30855  ordtconnlem1  31067  ddemeas  31395  omssubaddlem  31457  omssubadd  31458  eulerpartlemgvv  31534  tgoldbachgt  31834  bnj168  31900  bnj956  31948  bnj1098  31955  bnj1143  31962  bnj1146  31963  bnj1185  31965  bnj1196  31966  bnj600  32091  bnj849  32097  bnj906  32102  bnj916  32105  bnj983  32123  bnj984  32124  bnj1083  32148  bnj1176  32175  bnj1186  32177  bnj1189  32179  bnj1228  32181  bnj1253  32187  bnj1398  32204  bnj1463  32225  bnj1312  32228  bnj1514  32233  exdifsn  32243  lfuhgr3  32264  cusgredgex  32266  loop1cycl  32282  erdszelem10  32345  ptpconn  32378  coep  32885  coepr  32886  dffr5  32887  dfpo2  32889  opelco3  32916  dfon2lem8  32933  brimg  33296  dfrecs2  33309  dfrdg4  33310  ellines  33511  neifg  33617  bj-rexvw  34094  bj-snglc  34179  bj-snglss  34180  bj-rest10  34274  bj-restn0  34276  bj-restpw  34278  bj-rest0  34279  bj-restb  34280  bj-restuni  34283  bj-dfmpoa  34303  bj-finsumval0  34456  rnmptsn  34499  f1omptsnlem  34500  mptsnunlem  34502  topdifinffinlem  34511  isbasisrelowllem1  34519  isbasisrelowllem2  34520  relowlpssretop  34528  fvineqsneq  34576  pibt2  34581  poimirlem30  34804  abrexdom  34888  prdstotbnd  34955  eldmqsres2  35427  exanres  35435  rncnvepres  35444  rnxrnres  35529  1cossres  35556  eldm1cossres  35582  eldmqs1cossres  35775  prtlem17  35894  prter2  35899  islshpat  36035  lsat0cv  36051  lshpsmreu  36127  atex  36424  islpln5  36553  islvol5  36597  pmapglb  36788  pmapglb2N  36789  pmapglb2xN  36790  elpaddn0  36818  pmapjat1  36871  polval2N  36924  osumcllem11N  36984  pexmidlem8N  36995  cdlemftr3  37583  dibelval3  38165  dibglbN  38184  dicelval3  38198  dihglbcpreN  38318  dihglb2  38360  dihjatcclem4  38439  mapdordlem2  38655  mapdrvallem2  38663  mapdpglem3  38693  hdmapglem7a  38945  imaopab  38999  prjspeclsp  39142  rp-isfinite5  39763  rp-isfinite6  39764  elintima  39878  iunrelexpuztr  39944  cotrclrcl  39967  neik0pk1imk0  40277  ntrneineine0lem  40313  ntrneineine1lem  40314  ntrneiel2  40316  cpcolld  40474  expandrexn  40507  ismnuprim  40510  rr-grothprimbi  40511  rr-groth  40515  rexbidar  40658  onfrALTlem5  40756  onfrALTlem2  40760  onfrALTlem1  40762  onfrALTlem5VD  41099  onfrALTlem2VD  41103  onfrALTlem1VD  41104  chordthmALT  41147  rspcegf  41160  cncmpmax  41169  rfcnnnub  41173  inn0f  41215  nssrex  41231  eluni2f  41250  eliin2f  41251  suprnmpt  41310  founiiun0  41331  disjinfi  41334  fvelima2  41412  ssfiunibd  41456  infrpge  41499  fsumiunss  41736  islpcn  41800  lptre2pt  41801  stoweidlem14  42180  stoweidlem34  42200  stoweidlem35  42201  stoweidlem43  42209  stoweidlem44  42210  stoweidlem50  42216  stoweidlem54  42220  stoweidlem56  42222  stoweidlem59  42225  stoweidlem60  42226  fourier2  42393  qndenserrnbllem  42460  qndenserrn  42465  sge0rpcpnf  42584  hoidmvval0b  42753  hoiqssbllem3  42787  nfermltl8rev  43754  nfermltl2rev  43755  nfermltlrev  43756  nn0mnd  43933  opeliun2xp  44279  setrec1lem3  44690
  Copyright terms: Public domain W3C validator