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

Definition df-rex 2312
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 2307 . 2  wff  E. x  e.  A  ph
52cv 1242 . . . . 5  class  x
65, 3wcel 1393 . . . 4  wff  x  e.  A
76, 1wa 97 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wex 1381 . 2  wff  E. x
( x  e.  A  /\  ph )
94, 8wb 98 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  2316  rexnalim  2317  rexbida  2321  rexbidv2  2329  rexbii2  2335  r2exf  2342  risset  2352  nfrexdxy  2357  nfrexdya  2359  nfre1  2365  rexex  2368  rspe  2370  rsp2e  2372  rexim  2413  reximi2  2415  reximdv2  2418  r19.23t  2423  r19.41  2465  r19.43  2468  reean  2478  rexeqf  2502  reu5  2522  rmo5  2525  cbvrexf  2528  cbvrexdva2  2538  rexv  2572  2gencl  2587  3gencl  2588  rspce  2651  rspcimedv  2658  ceqsrexv  2674  rexab  2703  rexab2  2707  rexrab2  2708  morex  2725  reu2  2729  reu6  2730  reu3  2731  2reuswapdc  2743  2rmorex  2745  cbvrexcsf  2909  rexun  3123  reuss2  3217  reuun2  3220  reupick  3221  reupick3  3222  reximdva0m  3236  rabn0r  3244  rabn0m  3245  r19.2m  3309  r19.9rmv  3313  rexm  3320  rexsns  3409  rexsnsOLD  3410  exsnrex  3413  dfuni2  3582  eluni2  3584  elunirab  3593  iuncom4  3664  iunxiun  3736  intexrabim  3907  bnd2  3926  rexxfrd  4195  elxp2  4363  opeliunxp  4395  xpiundi  4398  xpiundir  4399  rexiunxp  4478  dmuni  4545  rnmpt  4582  elrnmpt1  4585  elres  4646  dfima2  4670  dfima3  4671  elima2  4674  dfco2a  4821  imaco  4826  imadiflem  4978  imadif  4979  imainlem  4980  imain  4981  funimaexglem  4982  fvelrnb  5221  rexrnmpt  5310  dffo4  5315  dffo5  5316  abrexco  5398  opabex3d  5748  opabex3  5749  abexssex  5752  abexex  5753  ecexr  6111  ltexnqq  6506  subhalfnqq  6512  ltbtwnnq  6514  nqnq0  6539  prnmaxl  6586  prnminu  6587  prarloc  6601  genpdflem  6605  genpassl  6622  genpassu  6623  nqprm  6640  nqprl  6649  nqpru  6650  ltsopr  6694  ltexprlemm  6698  ltexprlemloc  6705  axprecex  6954  axpre-ltirr  6956  2rexuz  8525  bdcuni  9996  bj-axun2  10035
  Copyright terms: Public domain W3C validator