Definition df-ral 1641

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 1637	. 2 wff A.x e. A ph
5	2	cv 952	. . . . 5 class x
6	5, 3	wcel 955	. . . 4 wff x e. A
7	6, 1	wi 3	. . 3 wff (x e. A -> ph)
8	7, 2	wal 951	. 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 1645  rexnal 1646  ralbida 1649  ralbidv2 1657  ralbii2 1663  r2al 1668  hbral 1678  hbra1 1679  r3al 1682  alral 1684  ra4 1686  rgen 1690  rgen2a 1691  r19.20 1694  r19.20i2 1695  r19.20da 1700  r19.20dv2 1703  r19.21ai 1704  r19.21t 1707  r19.21ad 1709  r19.21bi 1717  r19.22 1723  r19.23v 1733  r19.26 1742  r19.26m 1744  r19.27av 1746  r19.29 1748  rabid2 1762  ralcom2 1768  raleq1f 1775  cbvralf 1788  ralv 1811  rcla4 1862  reu2 1920  reu3 1921  reu6 1922  rmo4 1923  reu8 1926  2reuswap 1927  ra4sbc 1987  ra5 1990  dfss3 2049  dfss3f 2051  ssabral 2109  ss2rab 2113  rabss 2114  ssrab 2115  reuss2 2265  disj 2301  disj1 2302  r19.2z 2337  r19.3rzv 2338  ralidm 2347  ralf0 2349  ralpr 2418  unissb 2518  dfint2 2525  elint2 2530  elintrab 2535  ssintab 2540  dfiin2 2578  iunss 2581  ssiin 2589  dftr5 2673  sbcsng 2743  onminex 3010  dmopab3 3311  asymref 3423  asymref2 3424  asymrefOLD 3425  asymref2OLD 3426  dffun6 3525  funcnv 3543  funcnvuni 3550  zfrep6 3600  eqfnfv 3782  dff2 3802  dffo3 3804  cbvfo 3870  tfrlem2 3897  zfregcl 4567  zfinf 4598  ranksn 4661  scottexs 4690  scott0s 4691  kardex 4697  karden 4698  aceq1 4701  aceq2 4703  kmlem12 4748  kmlem14 4750  kmlem15 4751  zorn2lem4 4763  zorn2lem5 4764  zorn2lem7 4766  suplem1pr 5133  suplem2pr 5134  pre-axsup 5263  sup2 5998  infm3 6001  infmsup 6015  nnunb 6017  dfuz 6150  nnwof 6391  nnwos 6392  fz1sbct 6449  tgss3t 7580  indistop 7590  islp2 7688  cncnplem3 7715  cncfmet 7844  grothinf 8720  grothprim 8722  chsscm 9033  chcmh 9034  occont 9076  choc0 9205  h1deot 9387  pjnormss 10007  r19.3rzvb 10337  cmphmp 10408  qusp 10430  ismonc 10584

Copyright terms: Public domain