Definition df-ral 2513

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 2508	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1394	. . . . 5 class 𝑥
6	5, 3	wcel 2200	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1393	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 105	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is referenced by:  ralnex  2518  rexnalim  2519  dfrex2dc  2521  ralbida  2524  ralbidv2  2532  ralbid2  2534  ralbii2  2540  r2alf  2547  hbral  2559  hbra1  2560  nfra1  2561  nfraldw  2562  nfraldxy  2563  nfraldya  2565  r3al  2574  alral  2575  rsp  2577  rgen  2583  rgen2a  2584  ralim  2589  ralimi2  2590  ralimdaa  2596  ralimdv2  2600  ralrimi  2601  r19.21t  2605  ralrimd  2608  r19.21bi  2618  rexim  2624  r19.23t  2638  r19.26m  2662  r19.32r  2677  rabid2  2708  rabbi  2709  raleqf  2724  cbvralfw  2754  cbvralf  2756  cbvralvw  2769  cbvraldva2  2772  ralv  2818  ceqsralt  2828  rspct  2901  rspc  2902  rspcimdv  2909  rspc2gv  2920  ralab  2964  ralab2  2968  ralrab2  2969  reu2  2992  reu6  2993  reu3  2994  rmo4  2997  reu8  3000  rmo3f  3001  rmoim  3005  2reuswapdc  3008  2rmorex  3010  ra5  3119  rmo2ilem  3120  rmo3  3122  cbvralcsf  3188  dfss3  3214  dfss3f  3217  ssabral  3296  ss2rab  3301  rabss  3302  ssrab  3303  dfdif3  3315  ralunb  3386  reuss2  3485  rabeq0  3522  rabxmdc  3524  disj  3541  disj1  3543  r19.2m  3579  r19.2mOLD  3580  r19.3rm  3581  ralidm  3593  ralf0  3595  ralm  3596  ralsnsg  3704  ralsns  3705  unissb  3919  dfint2  3926  elint2  3931  elintrab  3936  ssintrab  3947  dfiin2g  3999  invdisj  4077  dftr5  4186  trint  4198  repizf2lem  4247  ordsucim  4594  ordunisuc2r  4608  setindel  4632  elirr  4635  en2lp  4648  zfregfr  4668  tfi  4676  zfinf2  4683  peano2  4689  peano5  4692  find  4693  raliunxp  4867  dmopab3  4940  issref  5115  asymref  5118  dffun7  5349  funcnv  5386  funcnvuni  5394  fnres  5444  fnopabg  5451  rexrnmpt  5784  dffo3  5788  acexmidlem2  6008  nfixpxy  6879  pw1dc0el  7094  isomnimap  7325  ismkvmap  7342  iswomnimap  7354  fz1sbc  10319  nnwosdc  12597  isprm2  12676  istopg  14710  cbvrald  16294  decidr  16302  bdcint  16382  bdcriota  16388  bj-axempty  16398  bj-indind  16437  bj-ssom  16441  findset  16450  bj-nnord  16463  bj-inf2vn  16479  bj-inf2vn2  16480  bj-findis  16484  alsconv  16594