Definition df-ral 1205

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 1201	. 2 wff A.x e. A ph
5	2	cv 1089	. . . . 5 class x
6	5, 3	wcel 1092	. . . 4 wff x e. A
7	6, 1	wi 2	. . 3 wff (x e. A -> ph)
8	7, 2	wal 672	. 2 wff A.x(x e. A -> ph)
9	4, 8	wb 127	1 wff (A.x e. A ph <-> A.x(x e. A -> ph))

This definition is referenced by:  ralnex 1209  rexnal 1210  biralda 1213  biraldv2 1221  birala 1228  r2al 1231  hbral 1236  hbra1 1237  r3al 1240  ra4 1243  rgen 1247  rgen2 1248  r19.20 1251  r19.20i2 1252  r19.20da 1255  r19.21ai 1258  r19.21v 1260  r19.21ad 1261  r19.21bi 1266  r19.22 1272  r19.23v 1282  r19.26 1289  r19.26m 1291  r19.27av 1293  r19.29 1295  rabid2 1309  ralcom2 1314  raleqf 1321  cbvralf 1330  reu2 1338  2reuswap 1341  ralv 1357  rcla4v 1402  rax4 1471  rax5 1472  dfss3 1498  dfss3f 1500  ss2rab 1553  disj 1733  disj1 1734  r19.2z 1766  r19.3rzv 1767  ralidm 1774  unissb 1941  dfint2 1967  elint2 1972  elintrab 1977  dfiin2 2015  iunss 2017  ssiin 2024  dftr5 2044  tfi 2244  onminex 2275  dmopab2 2541  dffun6 2687  funcnv 2703  funcnvuni 2706  zfrep6 2744  cleqfv 2880  cbvfo 2923  tfrlem2 2950  zfregcl 3446  zfinf 3474  ranksn 3532  scottexs 3543  scott0s 3544  kardex 3550  karden 3551  aceq1 3552  aceq2 3554  kmlem11 3590  kmlem14 3593  kmlem15 3594  zornlem5 3607  zornlem7 3609  suplem1pr 3955  suplem2pr 3956  axsup 4088  sup2 4510  nnunb 4520  nnwof 4609  nnwos 4610  zmin 4617  chsscm 5147  chcmh 5148  occont 5168  choc0 5291  h1deot 5454  h1det 5455  pjnormss 5638

metamath.org