Definition df-ral 1625

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 1621	. 2 wff A.x e. A ph
5	2	cv 1098	. . . . 5 class x
6	5, 3	wcel 1105	. . . 4 wff x e. A
7	6, 1	wi 3	. . 3 wff (x e. A -> ph)
8	7, 2	wal 950	. 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 1629  rexnal 1630  ralbida 1633  ralbidv2 1641  ralbii2 1647  r2al 1652  hbral 1662  hbra1 1663  r3al 1666  alral 1668  ra4 1670  rgen 1674  rgen2a 1675  r19.20 1678  r19.20i2 1679  r19.20da 1684  r19.20dv2 1687  r19.21ai 1688  r19.21t 1691  r19.21ad 1693  r19.21bi 1701  r19.22 1707  r19.23v 1717  r19.26 1726  r19.26m 1728  r19.27av 1730  r19.29 1732  rabid2 1746  ralcom2 1752  raleq1f 1759  cbvralf 1772  ralv 1795  rcla4 1844  reu2 1901  reu3 1902  reu6 1903  rmo4 1904  reu8 1907  2reuswap 1908  ra4sbc 1968  ra5 1971  dfss3 2030  dfss3f 2032  ssabral 2090  ss2rab 2094  rabss 2095  ssrab 2096  reuss2 2246  disj 2282  disj1 2283  r19.2z 2318  r19.3rzv 2319  ralidm 2328  ralf0 2330  ralpr 2399  unissb 2496  dfint2 2503  elint2 2508  elintrab 2513  ssintab 2518  dfiin2 2556  iunss 2559  ssiin 2567  dftr5 2651  sbcsng 2721  onminex 2983  dmopab3 3279  dffun6 3480  funcnv 3497  funcnvuni 3504  zfrep6 3554  eqfnfv 3736  dff2 3756  dffo3 3758  cbvfo 3824  tfrlem2 3851  zfregcl 4519  zfinf 4550  ranksn 4613  scottexs 4642  scott0s 4643  kardex 4649  karden 4650  aceq1 4653  aceq2 4655  kmlem12 4700  kmlem14 4702  kmlem15 4703  zorn2lem4 4715  zorn2lem5 4716  zorn2lem7 4718  suplem1pr 5084  suplem2pr 5085  pre-axsup 5214  sup2 5949  infm3 5952  infmsup 5966  nnunb 5968  dfuz 6101  nnwof 6342  nnwos 6343  fz1sbct 6400  tgss3t 7531  indistop 7541  islp2 7636  cncnplem3 7663  cncfmet 7792  grothinf 8633  grothprim 8635  r19.3rzvb 8697  cmphmp 8759  qusp 8780  ismonc 8934  chsscm 9263  chcmh 9264  occont 9290  choc0 9419  h1deot 9601  pjnormss 10221

Copyright terms: Public domain