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

Definition df-rex 2306
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 2301 . 2 wff x A φ
52cv 1241 . . . . 5 class x
65, 3wcel 1390 . . . 4 wff x A
76, 1wa 97 . . 3 wff (x A φ)
87, 2wex 1378 . 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  2310  rexnalim  2311  rexbida  2315  rexbidv2  2323  rexbii2  2329  r2exf  2336  risset  2346  nfrexdxy  2351  nfrexdya  2353  nfre1  2359  rexex  2362  rspe  2364  rsp2e  2366  rexim  2407  reximi2  2409  reximdv2  2412  r19.23t  2417  r19.41  2459  r19.43  2462  reean  2472  rexeqf  2496  reu5  2516  rmo5  2519  cbvrexf  2522  cbvrexdva2  2532  rexv  2566  2gencl  2581  3gencl  2582  rspce  2645  rspcimedv  2652  ceqsrexv  2668  rexab  2697  rexab2  2701  rexrab2  2702  morex  2719  reu2  2723  reu6  2724  reu3  2725  2reuswapdc  2737  2rmorex  2739  cbvrexcsf  2903  rexun  3117  reuss2  3211  reuun2  3214  reupick  3215  reupick3  3216  reximdva0m  3230  rabn0r  3238  rabn0m  3239  r19.2m  3303  r19.9rmv  3307  rexm  3314  rexsns  3400  rexsnsOLD  3401  exsnrex  3404  dfuni2  3573  eluni2  3575  elunirab  3584  iuncom4  3655  iunxiun  3727  intexrabim  3898  bnd2  3917  rexxfrd  4161  elxp2  4306  opeliunxp  4338  xpiundi  4341  xpiundir  4342  rexiunxp  4421  dmuni  4488  rnmpt  4525  elrnmpt1  4528  elres  4589  dfima2  4613  dfima3  4614  elima2  4617  dfco2a  4764  imaco  4769  imadiflem  4921  imadif  4922  imainlem  4923  imain  4924  funimaexglem  4925  fvelrnb  5164  rexrnmpt  5253  dffo4  5258  dffo5  5259  abrexco  5341  opabex3d  5690  opabex3  5691  abexssex  5694  abexex  5695  ecexr  6047  ltexnqq  6391  subhalfnqq  6397  ltbtwnnq  6399  nqnq0  6423  prnmaxl  6470  prnminu  6471  prarloc  6485  genpdflem  6489  genpassl  6507  genpassu  6508  nqprm  6525  ltsopr  6568  ltexprlemm  6572  ltexprlemloc  6579  axprecex  6724  axpre-ltirr  6726  2rexuz  8261  bdcuni  9265  bj-axun2  9300
  Copyright terms: Public domain W3C validator