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

Definition df-rex 2309
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 2304 . 2 wff 𝑥𝐴 𝜑
52cv 1242 . . . . 5 class 𝑥
65, 3wcel 1393 . . . 4 wff 𝑥𝐴
76, 1wa 97 . . 3 wff (𝑥𝐴𝜑)
87, 2wex 1381 . 2 wff 𝑥(𝑥𝐴𝜑)
94, 8wb 98 1 wff (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
Colors of variables: wff set class
This definition is referenced by:  ralnex  2313  rexnalim  2314  rexbida  2318  rexbidv2  2326  rexbii2  2332  r2exf  2339  risset  2349  nfrexdxy  2354  nfrexdya  2356  nfre1  2362  rexex  2365  rspe  2367  rsp2e  2369  rexim  2410  reximi2  2412  reximdv2  2415  r19.23t  2420  r19.41  2462  r19.43  2465  reean  2475  rexeqf  2499  reu5  2519  rmo5  2522  cbvrexf  2525  cbvrexdva2  2535  rexv  2569  2gencl  2584  3gencl  2585  rspce  2648  rspcimedv  2655  ceqsrexv  2671  rexab  2700  rexab2  2704  rexrab2  2705  morex  2722  reu2  2726  reu6  2727  reu3  2728  2reuswapdc  2740  2rmorex  2742  cbvrexcsf  2906  rexun  3120  reuss2  3214  reuun2  3217  reupick  3218  reupick3  3219  reximdva0m  3233  rabn0r  3241  rabn0m  3242  r19.2m  3306  r19.9rmv  3310  rexm  3317  rexsns  3406  rexsnsOLD  3407  exsnrex  3410  dfuni2  3579  eluni2  3581  elunirab  3590  iuncom4  3661  iunxiun  3733  intexrabim  3904  bnd2  3923  rexxfrd  4182  elxp2  4341  opeliunxp  4373  xpiundi  4376  xpiundir  4377  rexiunxp  4456  dmuni  4523  rnmpt  4560  elrnmpt1  4563  elres  4624  dfima2  4648  dfima3  4649  elima2  4652  dfco2a  4799  imaco  4804  imadiflem  4956  imadif  4957  imainlem  4958  imain  4959  funimaexglem  4960  fvelrnb  5199  rexrnmpt  5288  dffo4  5293  dffo5  5294  abrexco  5376  opabex3d  5726  opabex3  5727  abexssex  5730  abexex  5731  ecexr  6089  ltexnqq  6478  subhalfnqq  6484  ltbtwnnq  6486  nqnq0  6511  prnmaxl  6558  prnminu  6559  prarloc  6573  genpdflem  6577  genpassl  6594  genpassu  6595  nqprm  6612  nqprl  6621  nqpru  6622  ltsopr  6666  ltexprlemm  6670  ltexprlemloc  6677  axprecex  6926  axpre-ltirr  6928  2rexuz  8488  bdcuni  9860  bj-axun2  9899
  Copyright terms: Public domain W3C validator