Definition df-ral 2360

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	⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

Detailed syntax breakdown of Definition df-ral

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		cA	. . 3 class 𝐴
4	1, 2, 3	wral 2355	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1286	. . . . 5 class 𝑥
6	5, 3	wcel 1436	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1285	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 103	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is referenced by:  ralnex  2365  rexnalim  2366  dfrex2dc  2367  ralbida  2370  ralbidv2  2378  ralbii2  2384  r2alf  2391  hbral  2403  hbra1  2404  nfra1  2405  nfraldxy  2406  nfraldya  2408  r3al  2416  alral  2417  rsp  2419  rgen  2424  rgen2a  2425  ralim  2430  ralimi2  2431  ralimdaa  2436  ralimdv2  2439  ralrimi  2440  r19.21t  2444  ralrimd  2447  r19.21bi  2457  rexim  2463  r19.23t  2475  r19.26m  2496  r19.32r  2510  rabid2  2539  rabbi  2540  raleqf  2554  cbvralf  2580  cbvraldva2  2590  ralv  2630  ceqsralt  2640  rspct  2708  rspc  2709  rspcimdv  2716  rspc2gv  2725  ralab  2766  ralab2  2770  ralrab2  2771  reu2  2794  reu6  2795  reu3  2796  rmo4  2799  reu8  2802  rmoim  2805  2reuswapdc  2808  2rmorex  2810  ra5  2916  rmo2ilem  2917  rmo3  2919  cbvralcsf  2979  dfss3  3004  dfss3f  3006  ssabral  3081  ss2rab  3086  rabss  3087  ssrab  3088  dfdif3  3099  ralunb  3170  reuss2  3268  rabeq0  3301  rabxmdc  3303  disj  3319  disj1  3321  r19.2m  3356  r19.3rm  3357  ralidm  3369  rgenm  3371  ralf0  3372  ralm  3373  ralsnsg  3463  ralsns  3464  unissb  3666  dfint2  3673  elint2  3678  elintrab  3683  ssintrab  3694  dfiin2g  3746  invdisj  3815  dftr5  3914  trint  3926  repizf2lem  3971  ordsucim  4290  ordunisuc2r  4304  setindel  4327  elirr  4330  en2lp  4343  zfregfr  4362  tfi  4370  zfinf2  4377  peano2  4383  peano5  4386  find  4387  raliunxp  4545  dmopab3  4617  issref  4781  asymref  4784  dffun7  5007  funcnv  5040  funcnvuni  5048  fnres  5095  fnopabg  5102  rexrnmpt  5405  dffo3  5409  acexmidlem2  5610  isomnimap  6737  fz1sbc  9440  isprm2  10981  cbvrald  11133  decidr  11141  bdcint  11213  bdcriota  11219  bj-axempty  11229  bj-indind  11272  bj-ssom  11276  findset  11285  bj-nnord  11298  bj-inf2vn  11314  bj-inf2vn2  11315  bj-findis  11319  alsconv  11366