Definition df-ral 2917

Description: Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22. (Contributed by NM, 19-Aug-1993.)

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 setvar x
3		cA	. . 3 class A
4	1, 2, 3	wral 2912	. 2 wff A. x e. A ph
5	2	cv 1482	. . . . 5 class x
6	5, 3	wcel 1990	. . . 4 wff x e. A
7	6, 1	wi 4	. . 3 wff ( x e. A -> ph )
8	7, 2	wal 1481	. 2 wff A. x ( x e. A -> ph )
9	4, 8	wb 196	1 wff ( A. x e. A ph <-> A. x ( x e. A -> ph ) )

This definition is referenced by:  rgen  2922  alral  2928  rsp  2929  r2allem  2937  r3al  2940  nfra1  2941  hbral  2943  nfrald  2944  ral2imi  2947  ralimi2  2949  hbralrimi  2954  r19.21t  2955  ralrimd  2959  r19.21v  2960  ralimdv2  2961  rgen2a  2977  ralbii2  2978  ralbida  2982  ralbidv2  2984  raln  2991  ralnexOLD  2993  r19.23t  3021  r19.26m  3067  ralcom2  3104  rabid2  3118  rabid2f  3119  rabbi  3120  raleqf  3134  cbvralf  3165  cbvraldva2  3175  ralv  3219  ceqsralt  3229  rspct  3302  rspc  3303  rspcimdv  3310  rspc2gv  3321  ralxpxfr2d  3327  ralab  3367  ralab2  3371  ralrab2  3372  reu2  3394  reu6  3395  reu3  3396  rmo4  3399  reu8  3402  rmoim  3407  2reuswap  3410  2reu5lem2  3414  2reu5lem3  3415  rmo2  3526  rmo3  3528  cbvralcsf  3565  dfss3  3592  dfss3f  3595  ssabral  3673  ss2rab  3678  rabss  3679  ssrab  3680  ralunb  3794  reuss2  3907  n0el  3940  disj  4017  disj1  4019  r19.2z  4060  r19.3rz  4062  ralidm  4075  ralf0  4078  ralf0OLD  4079  falseral0  4081  rabsssn  4215  ralsnsg  4216  unissb  4469  dfint2  4477  elint2  4482  elintrab  4488  ssintrab  4500  dfiin2g  4553  invdisj  4638  disjss3  4652  dftr5  4755  trint  4768  reusv2lem4  4872  raliunxp  5261  dmopab3  5337  issref  5509  asymref  5512  asymref2  5513  dffun7  5915  funcnv  5958  fnres  6007  mptfnf  6015  fnopabg  6017  dff3  6372  dffo3  6374  find  7091  funcnvuni  7119  zfrep6  7134  nfixp  7927  marypha2lem3  8343  zfregcl  8499  zfregclOLD  8501  zfinf2  8539  scottexs  8750  scott0s  8751  aceq1  8940  aceq2  8942  kmlem12  8983  kmlem14  8985  kmlem15  8986  zorn2lem4  9321  zorn2lem5  9322  ingru  9637  axgroth5  9646  grothprim  9656  sstskm  9664  supsrlem  9932  infm3  10982  nnunb  11288  nnwos  11755  fz1sbc  12416  cotr2g  13715  caubnd  14098  rpnnen2lem12  14954  isprm2  15395  pgpfac1  18479  pgpfac  18483  lidldvgen  19255  iunocv  20025  istopg  20700  dfconn2  21222  1stccn  21266  iskgen3  21352  fbfinnfr  21645  iscmet3  23091  wilthlem3  24796  isch3  28098  choc0  28185  pjnormssi  29027  moel  29323  2reuswap2  29328  rmo3f  29335  rmo4fOLD  29336  ssiun3  29376  fmcncfil  29977  bnj115  30791  bnj538OLD  30810  bnj946  30845  bnj1142  30860  bnj1211  30868  bnj1294  30888  bnj1385  30903  bnj110  30928  bnj611  30988  bnj864  30992  bnj865  30993  bnj1000  31011  bnj978  31019  bnj1049  31042  bnj1090  31047  bnj1133  31057  bnj1176  31073  bnj1186  31075  bnj1253  31085  bnj1388  31101  untuni  31586  dfpo2  31645  dfon2lem8  31695  wzel  31771  wzelOLD  31772  dfrdg4  32058  onsuct0  32440  bj-ralvw  32865  bj-ralcom4  32868  bj-raldifsn  33054  bj-ismooredr  33064  poimirlem25  33434  poimirlem30  33439  nninfnub  33547  mptbi12f  33975  ralanid  34010  pmapglbx  35055  cdlemefrs29bpre0  35684  dford4  37596  cllem0  37871  elmapintrab  37882  elintima  37945  ss2iundf  37951  ntrneiiso  38389  ntrneik2  38390  ntrneix2  38391  ntrneikb  38392  ralbidar  38649  rexbidar  38650  ssralv2  38737  en3lpVD  39080  ssralv2VD  39102  trintALTVD  39116  ssrabf  39298  rabssf  39302  dffo3f  39364  rexrsb  41169  2rmoswap  41184  nrhmzr  41873  empty-surprise  42528  alsconv  42536