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

Definition df-ral 2396
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 2391 . 2  wff  A. x  e.  A  ph
52cv 1313 . . . . 5  class  x
65, 3wcel 1463 . . . 4  wff  x  e.  A
76, 1wi 4 . . 3  wff  ( x  e.  A  ->  ph )
87, 2wal 1312 . 2  wff  A. x
( x  e.  A  ->  ph )
94, 8wb 104 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  2401  rexnalim  2402  dfrex2dc  2403  ralbida  2406  ralbidv2  2414  ralbii2  2420  r2alf  2427  hbral  2439  hbra1  2440  nfra1  2441  nfraldxy  2442  nfraldya  2444  r3al  2452  alral  2453  rsp  2455  rgen  2460  rgen2a  2461  ralim  2466  ralimi2  2467  ralimdaa  2473  ralimdv2  2477  ralrimi  2478  r19.21t  2482  ralrimd  2485  r19.21bi  2495  rexim  2501  r19.23t  2514  r19.26m  2538  r19.32r  2553  rabid2  2582  rabbi  2583  raleqf  2597  cbvralf  2623  cbvraldva2  2633  ralv  2675  ceqsralt  2685  rspct  2754  rspc  2755  rspcimdv  2762  rspc2gv  2773  ralab  2815  ralab2  2819  ralrab2  2820  reu2  2843  reu6  2844  reu3  2845  rmo4  2848  reu8  2851  rmo3f  2852  rmoim  2856  2reuswapdc  2859  2rmorex  2861  ra5  2967  rmo2ilem  2968  rmo3  2970  cbvralcsf  3030  dfss3  3055  dfss3f  3057  ssabral  3136  ss2rab  3141  rabss  3142  ssrab  3143  dfdif3  3154  ralunb  3225  reuss2  3324  rabeq0  3360  rabxmdc  3362  disj  3379  disj1  3381  r19.2m  3417  r19.2mOLD  3418  r19.3rm  3419  ralidm  3431  rgenm  3433  ralf0  3434  ralm  3435  ralsnsg  3529  ralsns  3530  unissb  3734  dfint2  3741  elint2  3746  elintrab  3751  ssintrab  3762  dfiin2g  3814  invdisj  3891  dftr5  3997  trint  4009  repizf2lem  4053  ordsucim  4384  ordunisuc2r  4398  setindel  4421  elirr  4424  en2lp  4437  zfregfr  4456  tfi  4464  zfinf2  4471  peano2  4477  peano5  4480  find  4481  raliunxp  4648  dmopab3  4720  issref  4889  asymref  4892  dffun7  5118  funcnv  5152  funcnvuni  5160  fnres  5207  fnopabg  5214  rexrnmpt  5529  dffo3  5533  acexmidlem2  5737  nfixpxy  6577  isomnimap  6975  ismkvmap  6994  fz1sbc  9827  isprm2  11705  istopg  12072  cbvrald  12829  decidr  12837  bdcint  12909  bdcriota  12915  bj-axempty  12925  bj-indind  12964  bj-ssom  12968  findset  12977  bj-nnord  12990  bj-inf2vn  13006  bj-inf2vn2  13007  bj-findis  13011  alsconv  13084
  Copyright terms: Public domain W3C validator