ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-rex Structured version   GIF version

Definition df-rex 2282
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 (x A φx(x A φ))

Detailed syntax breakdown of Definition df-rex
StepHypRef Expression
1 wph . . 3 wff φ
2 vx . . 3 setvar x
3 cA . . 3 class A
41, 2, 3wrex 2277 . 2 wff x A φ
52cv 1223 . . . . 5 class x
65, 3wcel 1367 . . . 4 wff x A
76, 1wa 97 . . 3 wff (x A φ)
87, 2wex 1355 . 2 wff x(x A φ)
94, 8wb 98 1 wff (x A φx(x A φ))
Colors of variables: wff set class
This definition is referenced by:  ralnex  2286  rexnalim  2287  rexbida  2291  rexbidv2  2299  rexbii2  2305  r2exf  2312  risset  2322  nfrexdxy  2327  nfrexdya  2329  nfre1  2335  rexex  2338  rspe  2340  rsp2e  2342  rexim  2383  reximi2  2385  reximdv2  2388  r19.23t  2393  r19.41  2435  r19.43  2438  reean  2448  rexeqf  2472  reu5  2492  rmo5  2495  cbvrexf  2498  cbvrexdva2  2508  rexv  2541  2gencl  2556  3gencl  2557  rspce  2620  rspcimedv  2627  ceqsrexv  2643  rexab  2672  rexab2  2676  rexrab2  2677  morex  2694  reu2  2698  reu6  2699  reu3  2700  2reuswapdc  2712  2rmorex  2714  cbvrexcsf  2878  rexun  3092  reuss2  3186  reuun2  3189  reupick  3190  reupick3  3191  reximdva0m  3205  rabn0r  3213  rabn0m  3214  r19.2m  3278  r19.9rmv  3282  rexm  3289  rexsns  3373  rexsnsOLD  3374  exsnrex  3377  dfuni2  3546  eluni2  3548  elunirab  3557  iuncom4  3628  iunxiun  3700  intexrabim  3871  bnd2  3890  rexxfrd  4134  elxp2  4279  opeliunxp  4311  xpiundi  4314  xpiundir  4315  rexiunxp  4394  dmuni  4461  rnmpt  4498  elrnmpt1  4501  elres  4562  dfima2  4586  dfima3  4587  elima2  4590  dfco2a  4737  imaco  4742  imadiflem  4893  imadif  4894  imainlem  4895  imain  4896  funimaexglem  4897  fvelrnb  5135  rexrnmpt  5224  dffo4  5229  dffo5  5230  abrexco  5312  opabex3d  5660  opabex3  5661  abexssex  5664  abexex  5665  ecexr  6011  ltexnqq  6253  subhalfnqq  6258  ltbtwnnq  6260  nqnq0  6283  prnmaxl  6329  prnminu  6330  prarloc  6344  genpdflem  6348  genpassl  6366  genpassu  6367  nqprm  6384  ltsopr  6420  ltexprlemm  6424  ltexprlemloc  6431  axprecex  6570  axpre-ltirr  6572  bdcuni  8333  bj-axun2  8368
  Copyright terms: Public domain W3C validator