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

Definition df-ral 2398
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 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))

Detailed syntax breakdown of Definition df-ral
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
3 cA . . 3 class 𝐴
41, 2, 3wral 2393 . 2 wff 𝑥𝐴 𝜑
52cv 1315 . . . . 5 class 𝑥
65, 3wcel 1465 . . . 4 wff 𝑥𝐴
76, 1wi 4 . . 3 wff (𝑥𝐴𝜑)
87, 2wal 1314 . 2 wff 𝑥(𝑥𝐴𝜑)
94, 8wb 104 1 wff (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
Colors of variables: wff set class
This definition is referenced by:  ralnex  2403  rexnalim  2404  dfrex2dc  2405  ralbida  2408  ralbidv2  2416  ralbii2  2422  r2alf  2429  hbral  2441  hbra1  2442  nfra1  2443  nfraldxy  2444  nfraldya  2446  r3al  2454  alral  2455  rsp  2457  rgen  2462  rgen2a  2463  ralim  2468  ralimi2  2469  ralimdaa  2475  ralimdv2  2479  ralrimi  2480  r19.21t  2484  ralrimd  2487  r19.21bi  2497  rexim  2503  r19.23t  2516  r19.26m  2540  r19.32r  2555  rabid2  2584  rabbi  2585  raleqf  2599  cbvralf  2625  cbvraldva2  2635  ralv  2677  ceqsralt  2687  rspct  2756  rspc  2757  rspcimdv  2764  rspc2gv  2775  ralab  2817  ralab2  2821  ralrab2  2822  reu2  2845  reu6  2846  reu3  2847  rmo4  2850  reu8  2853  rmo3f  2854  rmoim  2858  2reuswapdc  2861  2rmorex  2863  ra5  2969  rmo2ilem  2970  rmo3  2972  cbvralcsf  3032  dfss3  3057  dfss3f  3059  ssabral  3138  ss2rab  3143  rabss  3144  ssrab  3145  dfdif3  3156  ralunb  3227  reuss2  3326  rabeq0  3362  rabxmdc  3364  disj  3381  disj1  3383  r19.2m  3419  r19.2mOLD  3420  r19.3rm  3421  ralidm  3433  rgenm  3435  ralf0  3436  ralm  3437  ralsnsg  3531  ralsns  3532  unissb  3736  dfint2  3743  elint2  3748  elintrab  3753  ssintrab  3764  dfiin2g  3816  invdisj  3893  dftr5  3999  trint  4011  repizf2lem  4055  ordsucim  4386  ordunisuc2r  4400  setindel  4423  elirr  4426  en2lp  4439  zfregfr  4458  tfi  4466  zfinf2  4473  peano2  4479  peano5  4482  find  4483  raliunxp  4650  dmopab3  4722  issref  4891  asymref  4894  dffun7  5120  funcnv  5154  funcnvuni  5162  fnres  5209  fnopabg  5216  rexrnmpt  5531  dffo3  5535  acexmidlem2  5739  nfixpxy  6579  isomnimap  6977  ismkvmap  6996  fz1sbc  9831  isprm2  11710  istopg  12077  cbvrald  12891  decidr  12899  bdcint  12971  bdcriota  12977  bj-axempty  12987  bj-indind  13026  bj-ssom  13030  findset  13039  bj-nnord  13052  bj-inf2vn  13068  bj-inf2vn2  13069  bj-findis  13073  alsconv  13141
  Copyright terms: Public domain W3C validator