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

Definition df-rex 2361
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 2356 . 2  wff  E. x  e.  A  ph
52cv 1286 . . . . 5  class  x
65, 3wcel 1436 . . . 4  wff  x  e.  A
76, 1wa 102 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wex 1424 . 2  wff  E. x
( x  e.  A  /\  ph )
94, 8wb 103 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  2365  rexnalim  2366  dfrex2dc  2367  rexbida  2371  rexbidv2  2379  rexbii2  2385  r2exf  2392  risset  2402  nfrexdxy  2407  nfrexdya  2409  nfre1  2415  rexex  2418  rspe  2420  rsp2e  2422  rexim  2463  reximi2  2465  reximdv2  2468  r19.23t  2475  r19.41  2518  r19.43  2521  reean  2531  rexeqf  2555  reu5  2575  rmo5  2578  cbvrexf  2581  cbvrexdva2  2591  rexv  2631  2gencl  2646  3gencl  2647  rspce  2710  rspcimedv  2717  ceqsrexv  2738  rexab  2768  rexab2  2772  rexrab2  2773  morex  2790  reu2  2794  reu6  2795  reu3  2796  2reuswapdc  2808  2rmorex  2810  cbvrexcsf  2980  rexun  3169  reuss2  3268  reuun2  3271  reupick  3272  reupick3  3273  reximdva0m  3287  rabn0r  3298  rabn0m  3299  r19.2m  3356  r19.9rmv  3360  rexm  3368  rexsns  3467  exsnrex  3470  dfuni2  3640  eluni2  3642  elunirab  3651  iuncom4  3722  iunxiun  3794  intexrabim  3966  bnd2  3985  rexxfrd  4261  elxp2  4431  opeliunxp  4463  xpiundi  4466  xpiundir  4467  rexiunxp  4548  dmuni  4616  rnmpt  4653  elrnmpt1  4656  elres  4717  dfima2  4745  dfima3  4746  elima2  4749  dfco2a  4899  imaco  4904  imadiflem  5060  imadif  5061  imainlem  5062  imain  5063  funimaexglem  5064  fvelrnb  5317  rexrnmpt  5407  dffo4  5412  dffo5  5413  abrexco  5501  opabex3d  5851  opabex3  5852  abexssex  5855  abexex  5856  ecexr  6251  mapsn  6401  mapsnen  6482  fimax2gtri  6571  ltexnqq  6914  subhalfnqq  6920  ltbtwnnq  6922  nqnq0  6947  prnmaxl  6994  prnminu  6995  prarloc  7009  genpdflem  7013  genpassl  7030  genpassu  7031  nqprm  7048  nqprl  7057  nqpru  7058  ltsopr  7102  ltexprlemm  7106  ltexprlemloc  7113  axprecex  7362  axpre-ltirr  7364  2rexuz  9005  ioom  9603  bdcuni  11236  bj-axun2  11275
  Copyright terms: Public domain W3C validator