Definition df-ral 2109

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 2105	. 2 wff A.x e. A ph
5	2	cv 1297	. . . . 5 class x
6	5, 3	wcel 1300	. . . 4 wff x e. A
7	6, 1	wi 3	. . 3 wff (x e. A -> ph)
8	7, 2	wal 1296	. 2 wff A.x(x e. A -> ph)
9	4, 8	wb 163	1 wff (A.x e. A ph <-> A.x(x e. A -> ph))

This definition is referenced by:  ralnex 2113  rexnal 2114  ralbida 2117  ralbidv2 2125  ralbii2 2131  r2al 2136  hbral 2146  hbra1 2147  hbra2 2148  r3al 2151  alral 2153  ra4 2155  rgen 2159  rgen2a 2160  rgen2aOLD 2161  ralim 2164  ralimi2 2165  ralimdaa 2170  ralimdv2 2173  r19.21ai 2174  r19.21t 2177  r19.21ad 2180  r19.21bi 2188  reximOLD 2195  r19.23 2206  r19.23OLD 2207  r19.26OLD 2220  r19.26m 2222  r19.27avOLD 2225  r19.29OLD 2228  ralcom2 2244  ralcom2OLD 2245  rabid2 2254  rabid2OLD 2255  raleqf 2263  cbvralf 2276  ralv 2305  rcla4 2373  rcla4OLD 2374  ralab 2417  ralrab 2418  reu2 2442  reu6 2443  reu3 2444  rmo4 2445  reu8 2448  2reuswap 2449  ra4sbc 2536  ra5 2539  dfss3 2611  dfss3f 2613  ssralv2 2674  ssabral 2678  ss2rab 2683  rabss 2684  ssrab 2685  ralunb 2784  reuss2 2870  disj 2914  disj1 2915  r19.2z 2958  r19.3rz 2960  r19.3rzv 2962  ralidm 2973  ralf0 2975  ralprg 3078  ralprOLD 3080  ralprOLDOLD 3081  raltp 3083  ralsng 3085  sbcsngOLD 3087  unissb 3208  dfint2 3216  elint2 3221  elinti 3223  elintrab 3228  ssintab 3233  ssintabOLD 3234  dfiin2g 3286  dfiin2OLD 3288  iunssOLD 3292  ssiinOLD 3303  iinxsng 3325  iinxprg 3326  dftr5 3414  truni 3425  trint 3426  eufromeq4 3831  onminex 3888  find 3977  dmopab3 4169  asymref 4308  asymrefOLD 4309  asymref2OLD 4311  dffun7 4447  funcnv 4475  funcnvuni 4482  zfrep6 4545  eqfnfv 4766  dff3 4790  dffo3 4792  cbvfo 4861  tfrlem2 5120  ordtypelem4 5687  ordtypelem6 5689  ordtypelem7 5690  zfregcl 5697  zfinf2 5732  en3lp 5758  ranksn 5800  scottexs 5848  scott0s 5849  aceq1 5891  aceq2 5893  kmlem12 5938  kmlem14 5940  kmlem15 5941  zorn2lem4 5953  zorn2lem5 5954  zorn2lem7 5956  suplem1pr 6313  suplem2pr 6314  pre-axsup 6444  sup2 7260  infm3 7263  infmsup 7277  nnunb 7279  dfuzi 7414  nnwof 7628  nnwos 7629  fz1sbc 7696  tgss3 8908  islp2 9023  cncnplem3 9053  cncfmet 9183  spwpr2 10001  axgroth5 10132  grothpw 10134  grothomex 10136  grothprim 10141  chsscmi 10745  chcmhi 10746  occon 10793  choc0 10923  h1deoi 11105  pjnormssi 11740  bnj10OLD 12375  bnj24 12388  bnj23 12397  bnj38 12409  bnj39OLD 12411  bnj47OLD 12418  bnj48OLD 12423  bnj55 12430  bnj58 12431  bnj112 12457  bnj115 12459  bnj228OLD 12518  bnj538 12534  bnj597 12558  bnj598 12559  bnj856 12789  bnj861 12794  bnj946 12845  bnj979 12863  bnj1058 12895  bnj1142 12940  bnj1156 12948  bnj1159 12951  bnj1183 12965  bnj1185 12967  bnj1211 12984  bnj1277 13034  bnj1289 13037  bnj611 13307  bnj965 13346  bnj1000 13364  bnj1137 13433  bnj1253 13470  bnj1283 13476  isprm2 13775  truniOLD 13792  trintOLD 13794  untuni 13797  ralunbOLD 13819  dfon2lem8 13856  predreseq 13890  trclss 13935  r19.3rzvb 14273  fates 14292  domfldrefc 14361  ranfldrefc 14362  domrngref 14364  ref4w 14370  imfstnrelc 14396  pospos 14635  cmphmp 14878  qusp 14908  fbaslim2 14936  bwt2 14960  ismonc 15163  isepic 15173  bpmp 15251  btmp 15252  dfiin2gOLD 15356  ordtypelem4OLD 15378  ordtypelem6OLD 15380  ordtypelem7OLD 15381  topbasfne 15499  neibastop1 15518  neibastop2 15523  neibastop3 15524  ralabOLD 15669  ralrabOLD 15670  nninfnub 15819  lmclim2 15850  heiborlem16 15970  n0el 16248  rcla4t 16407  cbvralcsf 16411  ralbidar 16422  rexbidar 16423  en3lpVD 16669  ssralv2VD 16690  trintALTVD 16704  pmapglbx 17251

Copyright terms: Public domain