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

Definition df-rex 2329
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  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)

Detailed syntax breakdown of Definition df-rex
StepHypRef Expression
1 wph . . 3  wff  ph
2 vx . . 3  setvar  x
3 cA . . 3  class  A
41, 2, 3wrex 2324 . 2  wff  E. x  e.  A  ph
52cv 1258 . . . . 5  class  x
65, 3wcel 1409 . . . 4  wff  x  e.  A
76, 1wa 101 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wex 1397 . 2  wff  E. x
( x  e.  A  /\  ph )
94, 8wb 102 1  wff  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
Colors of variables: wff set class
This definition is referenced by:  ralnex  2333  rexnalim  2334  rexbida  2338  rexbidv2  2346  rexbii2  2352  r2exf  2359  risset  2369  nfrexdxy  2374  nfrexdya  2376  nfre1  2382  rexex  2385  rspe  2387  rsp2e  2389  rexim  2430  reximi2  2432  reximdv2  2435  r19.23t  2440  r19.41  2482  r19.43  2485  reean  2495  rexeqf  2519  reu5  2539  rmo5  2542  cbvrexf  2545  cbvrexdva2  2555  rexv  2589  2gencl  2604  3gencl  2605  rspce  2668  rspcimedv  2675  ceqsrexv  2696  rexab  2725  rexab2  2729  rexrab2  2730  morex  2747  reu2  2751  reu6  2752  reu3  2753  2reuswapdc  2765  2rmorex  2767  cbvrexcsf  2936  rexun  3150  reuss2  3244  reuun2  3247  reupick  3248  reupick3  3249  reximdva0m  3263  rabn0r  3271  rabn0m  3272  r19.2m  3336  r19.9rmv  3340  rexm  3347  rexsns  3436  rexsnsOLD  3437  exsnrex  3440  dfuni2  3609  eluni2  3611  elunirab  3620  iuncom4  3691  iunxiun  3763  intexrabim  3934  bnd2  3953  rexxfrd  4222  elxp2  4390  opeliunxp  4422  xpiundi  4425  xpiundir  4426  rexiunxp  4505  dmuni  4572  rnmpt  4609  elrnmpt1  4612  elres  4673  dfima2  4697  dfima3  4698  elima2  4701  dfco2a  4848  imaco  4853  imadiflem  5005  imadif  5006  imainlem  5007  imain  5008  funimaexglem  5009  fvelrnb  5248  rexrnmpt  5337  dffo4  5342  dffo5  5343  abrexco  5425  opabex3d  5775  opabex3  5776  abexssex  5779  abexex  5780  ecexr  6141  ltexnqq  6563  subhalfnqq  6569  ltbtwnnq  6571  nqnq0  6596  prnmaxl  6643  prnminu  6644  prarloc  6658  genpdflem  6662  genpassl  6679  genpassu  6680  nqprm  6697  nqprl  6706  nqpru  6707  ltsopr  6751  ltexprlemm  6755  ltexprlemloc  6762  axprecex  7011  axpre-ltirr  7013  2rexuz  8620  ioom  9216  bdcuni  10369  bj-axun2  10408
  Copyright terms: Public domain W3C validator