Definition df-ral 1695

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

Assertion

Ref	Expression
df-ral	⊢ (∀x ∈ A φ ↔ ∀x(x ∈ A → φ))

Detailed syntax breakdown of Definition df-ral

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		vx	. . 3 set x
3		cA	. . 3 class A
4	1, 2, 3	wral 1691	. 2 wff ∀x ∈ A φ
5	2	cv 991	. . . . 5 class x
6	5, 3	wcel 994	. . . 4 wff x ∈ A
7	6, 1	wi 3	. . 3 wff (x ∈ A → φ)
8	7, 2	wal 990	. 2 wff ∀x(x ∈ A → φ)
9	4, 8	wb 144	1 wff (∀x ∈ A φ ↔ ∀x(x ∈ A → φ))

This definition is referenced by:  ralnex 1699  rexnal 1700  ralbida 1703  ralbidv2 1711  ralbii2 1717  r2al 1722  hbral 1732  hbra1 1733  r3al 1736  alral 1738  ra4 1740  rgen 1744  rgen2a 1745  r19.20 1748  r19.20i2 1749  r19.20da 1754  r19.20dv2 1757  r19.21ai 1758  r19.21t 1761  r19.21ad 1763  r19.21bi 1771  r19.22 1777  r19.23v 1787  r19.26 1796  r19.26m 1798  r19.27av 1800  r19.29 1802  rabid2 1816  ralcom2 1822  raleq1f 1829  cbvralf 1842  ralv 1866  rcla4 1917  reu2 1976  reu3 1977  reu6 1978  rmo4 1979  reu8 1982  2reuswap 1983  ra4sbc 2047  ra5 2050  dfss3 2111  dfss3f 2113  ssabral 2171  ss2rab 2175  rabss 2176  ssrab 2177  reuss2 2327  disj 2364  disj1 2365  r19.2z 2401  r19.3rzv 2402  ralidm 2411  ralf0 2413  ralpr 2486  ralsng 2489  sbcsng 2490  unissb 2595  dfint2 2602  elint2 2607  elintrab 2612  ssintab 2617  dfiin2 2656  iunss 2659  ssiin 2667  dftr5 2757  onminex 3164  dmopab3 3413  asymref 3531  asymref2 3532  dffun7 3644  funcnv 3662  funcnvuni 3669  zfrep6 3721  eqfnfv 3909  eqfnfv2 3911  dff3 3931  dffo3 3933  cbvfo 3999  tfrlem2 4213  zfregcl 4738  zfinf2 4771  ranksn 4835  scottexs 4864  scott0s 4865  kardex 4871  karden 4872  aceq1 4875  aceq2 4877  kmlem12 4922  kmlem14 4924  kmlem15 4925  zorn2lem4 4937  zorn2lem5 4938  zorn2lem7 4940  suplem1pr 5315  suplem2pr 5316  pre-axsup 5445  sup2 6219  infm3 6222  infmsup 6236  nnunb 6238  dfuzi 6373  nnwof 6586  nnwos 6587  fz1sbc 6648  tgss3 7850  islp2 7957  cncnplem3 7986  cncfmet 8116  spwpr2 8920  grothinf 9053  grothpw 9054  axgroth5 9055  grothprim 9057  chsscmi 9388  chcmhi 9389  occon 9436  choc0 9566  h1deoi 9748  pjnormssi 10376  r19.3rzvb 10721  domrngref 10764  ref3w 10772  imfstnrelc 10810  pospos 10882  cmphmp 11027  qusp 11068  bwt2 11123  ismonc 11269  isepic 11279  dfiin2g 11400  ordtypelem4 11430  ordtypelem6 11432  ordtypelem7 11433  topbasfne 11560  neibastop1 11579  neibastop2 11584  neibastop3 11585  nninfnub 11882  lmclim2 11915  heiborlem16 12026

Copyright terms: Public domain