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

Definition df-rex 2399
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 2394 . 2  wff  E. x  e.  A  ph
52cv 1315 . . . . 5  class  x
65, 3wcel 1465 . . . 4  wff  x  e.  A
76, 1wa 103 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wex 1453 . 2  wff  E. x
( x  e.  A  /\  ph )
94, 8wb 104 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  2403  rexnalim  2404  dfrex2dc  2405  rexbida  2409  rexbidv2  2417  rexbii2  2423  r2exf  2430  risset  2440  nfrexdxy  2445  nfrexdya  2447  nfre1  2453  rexex  2456  rspe  2458  rsp2e  2460  rexim  2503  reximi2  2505  reximdv2  2508  r19.23t  2516  r19.41  2563  r19.43  2566  reean  2576  rexeqf  2600  reu5  2620  rmo5  2623  cbvrexf  2626  cbvrexdva2  2636  rexv  2678  2gencl  2693  3gencl  2694  rspce  2758  rspcimedv  2765  ceqsrexv  2789  rexab  2819  rexab2  2823  rexrab2  2824  morex  2841  reu2  2845  reu6  2846  reu3  2847  2reuswapdc  2861  2rmorex  2863  cbvrexcsf  3033  ssrexf  3129  rexun  3226  reuss2  3326  reuun2  3329  reupick  3330  reupick3  3331  reximdva0m  3348  rabn0r  3359  rabn0m  3360  r19.2m  3419  r19.2mOLD  3420  r19.9rmv  3424  rexm  3432  rexsns  3533  exsnrex  3536  dfuni2  3708  eluni2  3710  elunirab  3719  iuncom4  3790  iunxiun  3864  intexrabim  4048  bnd2  4067  rexxfrd  4354  elxp2  4527  opeliunxp  4564  xpiundi  4567  xpiundir  4568  rexiunxp  4651  dmuni  4719  rnmpt  4757  elrnmpt1  4760  elres  4825  dfima2  4853  dfima3  4854  elima2  4857  dfco2a  5009  imaco  5014  imadiflem  5172  imadif  5173  imainlem  5174  imain  5175  funimaexglem  5176  fvelrnb  5437  rexrnmpt  5531  dffo4  5536  dffo5  5537  abrexco  5628  opabex3d  5987  opabex3  5988  abexssex  5991  abexex  5992  ecexr  6402  mapsn  6552  mapsnen  6673  fimax2gtri  6763  ctssdccl  6964  ltexnqq  7184  subhalfnqq  7190  ltbtwnnq  7192  nqnq0  7217  prnmaxl  7264  prnminu  7265  prarloc  7279  genpdflem  7283  genpassl  7300  genpassu  7301  nqprm  7318  nqprl  7327  nqpru  7328  ltsopr  7372  ltexprlemm  7376  ltexprlemloc  7383  suplocexprlemrl  7493  suplocexprlemloc  7497  axprecex  7656  axpre-ltirr  7658  sup3exmid  8679  2rexuz  9333  ioom  9993  inffinp1  11853  isbasis2g  12123  tgval2  12131  ntreq0  12212  bdcuni  12970  bj-axun2  13009
  Copyright terms: Public domain W3C validator