Definition df-ral 2308

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

This definition is referenced by:  ralnex  2313  rexnalim  2314  ralbida  2317  ralbidv2  2325  ralbii2  2331  r2alf  2338  hbral  2350  hbra1  2351  nfra1  2352  nfraldxy  2353  nfraldya  2355  r3al  2363  alral  2364  rsp  2366  rgen  2371  rgen2a  2372  ralim  2377  ralimi2  2378  ralimdaa  2383  ralimdv2  2386  ralrimi  2387  r19.21t  2391  ralrimd  2394  r19.21bi  2404  rexim  2410  r19.23t  2420  r19.26m  2441  r19.32r  2454  rabid2  2483  rabbi  2484  raleqf  2498  cbvralf  2524  cbvraldva2  2534  ralv  2568  ceqsralt  2578  rspct  2646  rspc  2647  rspcimdv  2654  ralab  2698  ralab2  2702  ralrab2  2703  reu2  2726  reu6  2727  reu3  2728  rmo4  2731  reu8  2734  rmoim  2737  2reuswapdc  2740  2rmorex  2742  ra5  2843  rmo2ilem  2844  rmo3  2846  cbvralcsf  2905  dfss3  2932  dfss3f  2934  ssabral  3008  ss2rab  3013  rabss  3014  ssrab  3015  ralunb  3121  reuss2  3214  rabeq0  3244  rabxmdc  3246  disj  3265  disj1  3267  r19.2m  3306  r19.3rm  3307  ralidm  3318  rgenm  3320  ralf0  3321  ralm  3322  ralsnsg  3404  ralsns  3405  unissb  3607  dfint2  3614  elint2  3619  elintrab  3624  ssintrab  3635  dfiin2g  3687  invdisj  3756  dftr5  3854  trint  3866  repizf2lem  3911  ordsucim  4213  ordunisuc2r  4227  setindel  4248  elirr  4251  en2lp  4263  tfi  4283  zfinf2  4290  peano2  4296  peano5  4299  find  4300  raliunxp  4455  dmopab3  4526  issref  4685  asymref  4688  dffun7  4906  funcnv  4938  funcnvuni  4946  fnres  4993  fnopabg  5000  rexrnmpt  5288  dffo3  5292  acexmidlem2  5487  fz1sbc  8916  cbvrald  9791  bdcint  9861  bdcriota  9867  bj-axempty  9877  bj-indind  9920  bj-ssom  9924  peano5setOLD  9929  findset  9934  bj-nnord  9947  bj-inf2vn  9963  bj-inf2vn2  9964  bj-findis  9968  alsconv  9982