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

Definition df-rex 2286
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 2281 . 2 wff x A φ
52cv 1225 . . . . 5 class x
65, 3wcel 1370 . . . 4 wff x A
76, 1wa 97 . . 3 wff (x A φ)
87, 2wex 1358 . 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  2290  rexnalim  2291  rexbida  2295  rexbidv2  2303  rexbii2  2309  r2exf  2316  risset  2326  nfrexdxy  2331  nfrexdya  2333  nfre1  2339  rexex  2342  rspe  2344  rsp2e  2346  rexim  2387  reximi2  2389  reximdv2  2392  r19.23t  2397  r19.41  2439  r19.43  2442  reean  2452  rexeqf  2476  reu5  2496  rmo5  2499  cbvrexf  2502  cbvrexdva2  2512  rexv  2545  2gencl  2560  3gencl  2561  rspce  2624  rspcimedv  2631  ceqsrexv  2647  rexab  2676  rexab2  2680  rexrab2  2681  morex  2698  reu2  2702  reu6  2703  reu3  2704  2reuswapdc  2716  2rmorex  2718  cbvrexcsf  2882  rexun  3096  reuss2  3190  reuun2  3193  reupick  3194  reupick3  3195  reximdva0m  3209  rabn0r  3217  rabn0m  3218  r19.2m  3282  r19.9rmv  3287  rexm  3295  rexsns  3379  rexsnsOLD  3380  exsnrex  3383  dfuni2  3552  eluni2  3554  elunirab  3563  iuncom4  3634  iunxiun  3706  intexrabim  3877  bnd2  3896  rexxfrd  4141  elxp2  4286  opeliunxp  4318  xpiundi  4321  xpiundir  4322  rexiunxp  4401  dmuni  4468  rnmpt  4505  elrnmpt1  4508  elres  4569  dfima2  4593  dfima3  4594  elima2  4597  dfco2a  4744  imaco  4749  imadiflem  4900  imadif  4901  imainlem  4902  imain  4903  funimaexglem  4904  fvelrnb  5142  rexrnmpt  5231  dffo4  5236  dffo5  5237  abrexco  5319  opabex3d  5667  opabex3  5668  abexssex  5671  abexex  5672  ecexr  6018  ltexnqq  6260  subhalfnqq  6265  ltbtwnnq  6267  nqnq0  6290  prnmaxl  6336  prnminu  6337  prarloc  6351  genpdflem  6355  genpassl  6373  genpassu  6374  nqprm  6391  ltsopr  6427  ltexprlemm  6431  ltexprlemloc  6438  axprecex  6568  axpre-ltirr  6570  bdcuni  7242  bj-axun2  7277
  Copyright terms: Public domain W3C validator