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

Definition df-ral 2421
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 2416 . 2 wff 𝑥𝐴 𝜑
52cv 1330 . . . . 5 class 𝑥
65, 3wcel 1480 . . . 4 wff 𝑥𝐴
76, 1wi 4 . . 3 wff (𝑥𝐴𝜑)
87, 2wal 1329 . 2 wff 𝑥(𝑥𝐴𝜑)
94, 8wb 104 1 wff (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
Colors of variables: wff set class
This definition is referenced by:  ralnex  2426  rexnalim  2427  dfrex2dc  2428  ralbida  2431  ralbidv2  2439  ralbii2  2445  r2alf  2452  hbral  2464  hbra1  2465  nfra1  2466  nfraldxy  2467  nfraldya  2469  r3al  2477  alral  2478  rsp  2480  rgen  2485  rgen2a  2486  ralim  2491  ralimi2  2492  ralimdaa  2498  ralimdv2  2502  ralrimi  2503  r19.21t  2507  ralrimd  2510  r19.21bi  2520  rexim  2526  r19.23t  2539  r19.26m  2563  r19.32r  2578  rabid2  2607  rabbi  2608  raleqf  2622  cbvralf  2648  cbvraldva2  2661  ralv  2703  ceqsralt  2713  rspct  2782  rspc  2783  rspcimdv  2790  rspc2gv  2801  ralab  2844  ralab2  2848  ralrab2  2849  reu2  2872  reu6  2873  reu3  2874  rmo4  2877  reu8  2880  rmo3f  2881  rmoim  2885  2reuswapdc  2888  2rmorex  2890  ra5  2997  rmo2ilem  2998  rmo3  3000  cbvralcsf  3062  dfss3  3087  dfss3f  3089  ssabral  3168  ss2rab  3173  rabss  3174  ssrab  3175  dfdif3  3186  ralunb  3257  reuss2  3356  rabeq0  3392  rabxmdc  3394  disj  3411  disj1  3413  r19.2m  3449  r19.2mOLD  3450  r19.3rm  3451  ralidm  3463  rgenm  3465  ralf0  3466  ralm  3467  ralsnsg  3561  ralsns  3562  unissb  3766  dfint2  3773  elint2  3778  elintrab  3783  ssintrab  3794  dfiin2g  3846  invdisj  3923  dftr5  4029  trint  4041  repizf2lem  4085  ordsucim  4416  ordunisuc2r  4430  setindel  4453  elirr  4456  en2lp  4469  zfregfr  4488  tfi  4496  zfinf2  4503  peano2  4509  peano5  4512  find  4513  raliunxp  4680  dmopab3  4752  issref  4921  asymref  4924  dffun7  5150  funcnv  5184  funcnvuni  5192  fnres  5239  fnopabg  5246  rexrnmpt  5563  dffo3  5567  acexmidlem2  5771  nfixpxy  6611  isomnimap  7009  ismkvmap  7028  iswomnimap  7038  fz1sbc  9888  isprm2  11809  istopg  12180  cbvrald  13079  decidr  13087  bdcint  13159  bdcriota  13165  bj-axempty  13175  bj-indind  13214  bj-ssom  13218  findset  13227  bj-nnord  13240  bj-inf2vn  13256  bj-inf2vn2  13257  bj-findis  13261  alsconv  13337
  Copyright terms: Public domain W3C validator