Definition df-ral 1649

Description: Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22.

Assertion

Ref	Expression
df-ral	|- (A.x e. A ph <-> A.x(x e. A -> ph))

Detailed syntax breakdown of Definition df-ral

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 set x
3		cA	. . 3 class A
4	1, 2, 3	wral 1645	. 2 wff A.x e. A ph
5	2	cv 955	. . . . 5 class x
6	5, 3	wcel 958	. . . 4 wff x e. A
7	6, 1	wi 3	. . 3 wff (x e. A -> ph)
8	7, 2	wal 954	. 2 wff A.x(x e. A -> ph)
9	4, 8	wb 146	1 wff (A.x e. A ph <-> A.x(x e. A -> ph))

This definition is referenced by:  ralnex 1653  rexnal 1654  ralbida 1657  ralbidv2 1665  ralbii2 1671  r2al 1676  hbral 1686  hbra1 1687  r3al 1690  alral 1692  ra4 1694  rgen 1698  rgen2a 1699  r19.20 1702  r19.20i2 1703  r19.20da 1708  r19.20dv2 1711  r19.21ai 1712  r19.21t 1715  r19.21ad 1717  r19.21bi 1725  r19.22 1731  r19.23v 1741  r19.26 1750  r19.26m 1752  r19.27av 1754  r19.29 1756  rabid2 1770  ralcom2 1776  raleq1f 1783  cbvralf 1796  ralv 1820  rcla4 1871  reu2 1930  reu3 1931  reu6 1932  rmo4 1933  reu8 1936  2reuswap 1937  ra4sbc 1997  ra5 2000  dfss3 2059  dfss3f 2061  ssabral 2119  ss2rab 2123  rabss 2124  ssrab 2125  reuss2 2275  disj 2311  disj1 2312  r19.2z 2347  r19.3rzv 2348  ralidm 2357  ralf0 2359  ralpr 2428  unissb 2528  dfint2 2535  elint2 2540  elintrab 2545  ssintab 2550  dfiin2 2588  iunss 2591  ssiin 2599  dftr5 2683  sbcsng 2753  onminex 3020  dmopab3 3322  asymref 3439  asymref2 3440  dffun6 3539  funcnv 3557  funcnvuni 3564  zfrep6 3614  eqfnfv 3797  dff2 3817  dffo3 3819  cbvfo 3885  tfrlem2 3912  zfregcl 4595  zfinf 4626  ranksn 4689  scottexs 4718  scott0s 4719  kardex 4725  karden 4726  aceq1 4729  aceq2 4731  kmlem12 4776  kmlem14 4778  kmlem15 4779  zorn2lem4 4791  zorn2lem5 4792  zorn2lem7 4794  suplem1pr 5161  suplem2pr 5162  pre-axsup 5291  sup2 6051  infm3 6054  infmsup 6068  nnunb 6070  dfuz 6202  nnwof 6459  nnwos 6460  fz1sbct 6517  tgss3t 7638  indistop 7648  islp2 7747  cncnplem3 7776  cncfmet 7905  spwpr2 8658  grothinf 8781  grothprim 8783  chsscm 9112  chcmh 9113  occont 9160  choc0 9290  h1deot 9472  pjnormss 10096  r19.3rzvb 10437  cmphmp 10521  qusp 10555  ismonc 10742

Copyright terms: Public domain