Definition df-ral 1646

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 1642	. 2 wff ∀x ∈ A φ
5	2	cv 953	. . . . 5 class x
6	5, 3	wcel 956	. . . 4 wff x ∈ A
7	6, 1	wi 3	. . 3 wff (x ∈ A → φ)
8	7, 2	wal 952	. 2 wff ∀x(x ∈ A → φ)
9	4, 8	wb 146	1 wff (∀x ∈ A φ ↔ ∀x(x ∈ A → φ))

This definition is referenced by:  ralnex 1650  rexnal 1651  ralbida 1654  ralbidv2 1662  ralbii2 1668  r2al 1673  hbral 1683  hbra1 1684  r3al 1687  alral 1689  ra4 1691  rgen 1695  rgen2a 1696  r19.20 1699  r19.20i2 1700  r19.20da 1705  r19.20dv2 1708  r19.21ai 1709  r19.21t 1712  r19.21ad 1714  r19.21bi 1722  r19.22 1728  r19.23v 1738  r19.26 1747  r19.26m 1749  r19.27av 1751  r19.29 1753  rabid2 1767  ralcom2 1773  raleq1f 1780  cbvralf 1793  ralv 1816  rcla4 1867  reu2 1926  reu3 1927  reu6 1928  rmo4 1929  reu8 1932  2reuswap 1933  ra4sbc 1993  ra5 1996  dfss3 2055  dfss3f 2057  ssabral 2115  ss2rab 2119  rabss 2120  ssrab 2121  reuss2 2271  disj 2307  disj1 2308  r19.2z 2343  r19.3rzv 2344  ralidm 2353  ralf0 2355  ralpr 2424  unissb 2523  dfint2 2530  elint2 2535  elintrab 2540  ssintab 2545  dfiin2 2583  iunss 2586  ssiin 2594  dftr5 2678  sbcsng 2748  onminex 3015  dmopab3 3317  asymref 3431  asymref2 3432  dffun6 3531  funcnv 3549  funcnvuni 3556  zfrep6 3606  eqfnfv 3788  dff2 3808  dffo3 3810  cbvfo 3876  tfrlem2 3903  zfregcl 4575  zfinf 4606  ranksn 4669  scottexs 4698  scott0s 4699  kardex 4705  karden 4706  aceq1 4709  aceq2 4711  kmlem12 4756  kmlem14 4758  kmlem15 4759  zorn2lem4 4771  zorn2lem5 4772  zorn2lem7 4774  suplem1pr 5141  suplem2pr 5142  pre-axsup 5271  sup2 6006  infm3 6009  infmsup 6023  nnunb 6025  dfuz 6158  nnwof 6399  nnwos 6400  fz1sbct 6457  tgss3t 7588  indistop 7598  islp2 7697  cncnplem3 7726  cncfmet 7857  grothinf 8720  grothprim 8722  chsscm 9051  chcmh 9052  occont 9099  choc0 9228  h1deot 9410  pjnormss 10034  r19.3rzvb 10373  cmphmp 10444  qusp 10466  ismonc 10620

Copyright terms: Public domain