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

Definition df-rex 2355
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 2350 . 2 wff 𝑥𝐴 𝜑
52cv 1284 . . . . 5 class 𝑥
65, 3wcel 1434 . . . 4 wff 𝑥𝐴
76, 1wa 102 . . 3 wff (𝑥𝐴𝜑)
87, 2wex 1422 . 2 wff 𝑥(𝑥𝐴𝜑)
94, 8wb 103 1 wff (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
Colors of variables: wff set class
This definition is referenced by:  ralnex  2359  rexnalim  2360  rexbida  2364  rexbidv2  2372  rexbii2  2378  r2exf  2385  risset  2395  nfrexdxy  2400  nfrexdya  2402  nfre1  2408  rexex  2411  rspe  2413  rsp2e  2415  rexim  2456  reximi2  2458  reximdv2  2461  r19.23t  2468  r19.41  2510  r19.43  2513  reean  2523  rexeqf  2547  reu5  2567  rmo5  2570  cbvrexf  2573  cbvrexdva2  2583  rexv  2618  2gencl  2633  3gencl  2634  rspce  2697  rspcimedv  2704  ceqsrexv  2726  rexab  2755  rexab2  2759  rexrab2  2760  morex  2777  reu2  2781  reu6  2782  reu3  2783  2reuswapdc  2795  2rmorex  2797  cbvrexcsf  2966  rexun  3153  reuss2  3251  reuun2  3254  reupick  3255  reupick3  3256  reximdva0m  3270  rabn0r  3278  rabn0m  3279  r19.2m  3336  r19.9rmv  3340  rexm  3348  rexsns  3440  exsnrex  3443  dfuni2  3611  eluni2  3613  elunirab  3622  iuncom4  3693  iunxiun  3765  intexrabim  3936  bnd2  3955  rexxfrd  4221  elxp2  4389  opeliunxp  4421  xpiundi  4424  xpiundir  4425  rexiunxp  4506  dmuni  4573  rnmpt  4610  elrnmpt1  4613  elres  4674  dfima2  4700  dfima3  4701  elima2  4704  dfco2a  4851  imaco  4856  imadiflem  5009  imadif  5010  imainlem  5011  imain  5012  funimaexglem  5013  fvelrnb  5253  rexrnmpt  5342  dffo4  5347  dffo5  5348  abrexco  5430  opabex3d  5779  opabex3  5780  abexssex  5783  abexex  5784  ecexr  6177  ltexnqq  6660  subhalfnqq  6666  ltbtwnnq  6668  nqnq0  6693  prnmaxl  6740  prnminu  6741  prarloc  6755  genpdflem  6759  genpassl  6776  genpassu  6777  nqprm  6794  nqprl  6803  nqpru  6804  ltsopr  6848  ltexprlemm  6852  ltexprlemloc  6859  axprecex  7108  axpre-ltirr  7110  2rexuz  8751  ioom  9347  bdcuni  10825  bj-axun2  10864
  Copyright terms: Public domain W3C validator