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

Definition df-ral 2328
Description: Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22. (Contributed by NM, 19-Aug-1993.)
Assertion
Ref Expression
df-ral  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )

Detailed syntax breakdown of Definition df-ral
StepHypRef Expression
1 wph . . 3  wff  ph
2 vx . . 3  setvar  x
3 cA . . 3  class  A
41, 2, 3wral 2323 . 2  wff  A. x  e.  A  ph
52cv 1258 . . . . 5  class  x
65, 3wcel 1409 . . . 4  wff  x  e.  A
76, 1wi 4 . . 3  wff  ( x  e.  A  ->  ph )
87, 2wal 1257 . 2  wff  A. x
( x  e.  A  ->  ph )
94, 8wb 102 1  wff  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
Colors of variables: wff set class
This definition is referenced by:  ralnex  2333  rexnalim  2334  ralbida  2337  ralbidv2  2345  ralbii2  2351  r2alf  2358  hbral  2370  hbra1  2371  nfra1  2372  nfraldxy  2373  nfraldya  2375  r3al  2383  alral  2384  rsp  2386  rgen  2391  rgen2a  2392  ralim  2397  ralimi2  2398  ralimdaa  2403  ralimdv2  2406  ralrimi  2407  r19.21t  2411  ralrimd  2414  r19.21bi  2424  rexim  2430  r19.23t  2440  r19.26m  2461  r19.32r  2474  rabid2  2503  rabbi  2504  raleqf  2518  cbvralf  2544  cbvraldva2  2554  ralv  2588  ceqsralt  2598  rspct  2666  rspc  2667  rspcimdv  2674  ralab  2723  ralab2  2727  ralrab2  2728  reu2  2751  reu6  2752  reu3  2753  rmo4  2756  reu8  2759  rmoim  2762  2reuswapdc  2765  2rmorex  2767  ra5  2873  rmo2ilem  2874  rmo3  2876  cbvralcsf  2935  dfss3  2962  dfss3f  2964  ssabral  3038  ss2rab  3043  rabss  3044  ssrab  3045  ralunb  3151  reuss2  3244  rabeq0  3274  rabxmdc  3276  disj  3295  disj1  3297  r19.2m  3336  r19.3rm  3337  ralidm  3348  rgenm  3350  ralf0  3351  ralm  3352  ralsnsg  3434  ralsns  3435  unissb  3637  dfint2  3644  elint2  3649  elintrab  3654  ssintrab  3665  dfiin2g  3717  invdisj  3786  dftr5  3884  trint  3896  repizf2lem  3941  ordsucim  4253  ordunisuc2r  4267  setindel  4290  elirr  4293  en2lp  4305  zfregfr  4325  tfi  4332  zfinf2  4339  peano2  4345  peano5  4348  find  4349  raliunxp  4504  dmopab3  4575  issref  4734  asymref  4737  dffun7  4955  funcnv  4987  funcnvuni  4995  fnres  5042  fnopabg  5049  rexrnmpt  5337  dffo3  5341  acexmidlem2  5536  fz1sbc  9059  cbvrald  10300  bdcint  10370  bdcriota  10376  bj-axempty  10386  bj-indind  10429  bj-ssom  10433  peano5setOLD  10438  findset  10443  bj-nnord  10456  bj-inf2vn  10472  bj-inf2vn2  10473  bj-findis  10477  alsconv  10492
  Copyright terms: Public domain W3C validator