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

Definition df-rex 2359
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 2354 . 2  wff  E. x  e.  A  ph
52cv 1284 . . . . 5  class  x
65, 3wcel 1434 . . . 4  wff  x  e.  A
76, 1wa 102 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wex 1422 . 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  2363  rexnalim  2364  dfrex2dc  2365  rexbida  2369  rexbidv2  2377  rexbii2  2383  r2exf  2390  risset  2400  nfrexdxy  2405  nfrexdya  2407  nfre1  2413  rexex  2416  rspe  2418  rsp2e  2420  rexim  2461  reximi2  2463  reximdv2  2466  r19.23t  2473  r19.41  2515  r19.43  2518  reean  2528  rexeqf  2552  reu5  2572  rmo5  2575  cbvrexf  2578  cbvrexdva2  2588  rexv  2628  2gencl  2643  3gencl  2644  rspce  2707  rspcimedv  2714  ceqsrexv  2735  rexab  2765  rexab2  2769  rexrab2  2770  morex  2787  reu2  2791  reu6  2792  reu3  2793  2reuswapdc  2805  2rmorex  2807  cbvrexcsf  2976  rexun  3164  reuss2  3262  reuun2  3265  reupick  3266  reupick3  3267  reximdva0m  3281  rabn0r  3292  rabn0m  3293  r19.2m  3350  r19.9rmv  3354  rexm  3362  rexsns  3456  exsnrex  3459  dfuni2  3629  eluni2  3631  elunirab  3640  iuncom4  3711  iunxiun  3783  intexrabim  3954  bnd2  3973  rexxfrd  4248  elxp2  4418  opeliunxp  4450  xpiundi  4453  xpiundir  4454  rexiunxp  4535  dmuni  4603  rnmpt  4640  elrnmpt1  4643  elres  4704  dfima2  4730  dfima3  4731  elima2  4734  dfco2a  4884  imaco  4889  imadiflem  5045  imadif  5046  imainlem  5047  imain  5048  funimaexglem  5049  fvelrnb  5296  rexrnmpt  5386  dffo4  5391  dffo5  5392  abrexco  5477  opabex3d  5826  opabex3  5827  abexssex  5830  abexex  5831  ecexr  6226  mapsn  6376  mapsnen  6457  ltexnqq  6869  subhalfnqq  6875  ltbtwnnq  6877  nqnq0  6902  prnmaxl  6949  prnminu  6950  prarloc  6964  genpdflem  6968  genpassl  6985  genpassu  6986  nqprm  7003  nqprl  7012  nqpru  7013  ltsopr  7057  ltexprlemm  7061  ltexprlemloc  7068  axprecex  7317  axpre-ltirr  7319  2rexuz  8964  ioom  9560  bdcuni  11109  bj-axun2  11148
  Copyright terms: Public domain W3C validator