Definition df-ral 2311

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 2306	. 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  2316  rexnalim  2317  ralbida  2320  ralbidv2  2328  ralbii2  2334  r2alf  2341  hbral  2353  hbra1  2354  nfra1  2355  nfraldxy  2356  nfraldya  2358  r3al  2366  alral  2367  rsp  2369  rgen  2374  rgen2a  2375  ralim  2380  ralimi2  2381  ralimdaa  2386  ralimdv2  2389  ralrimi  2390  r19.21t  2394  ralrimd  2397  r19.21bi  2407  rexim  2413  r19.23t  2423  r19.26m  2444  r19.32r  2457  rabid2  2486  rabbi  2487  raleqf  2501  cbvralf  2527  cbvraldva2  2537  ralv  2571  ceqsralt  2581  rspct  2649  rspc  2650  rspcimdv  2657  ralab  2701  ralab2  2705  ralrab2  2706  reu2  2729  reu6  2730  reu3  2731  rmo4  2734  reu8  2737  rmoim  2740  2reuswapdc  2743  2rmorex  2745  ra5  2846  rmo2ilem  2847  rmo3  2849  cbvralcsf  2908  dfss3  2935  dfss3f  2937  ssabral  3011  ss2rab  3016  rabss  3017  ssrab  3018  ralunb  3124  reuss2  3217  rabeq0  3247  rabxmdc  3249  disj  3268  disj1  3270  r19.2m  3309  r19.3rm  3310  ralidm  3321  rgenm  3323  ralf0  3324  ralm  3325  ralsnsg  3407  ralsns  3408  unissb  3610  dfint2  3617  elint2  3622  elintrab  3627  ssintrab  3638  dfiin2g  3690  invdisj  3759  dftr5  3857  trint  3869  repizf2lem  3914  ordsucim  4226  ordunisuc2r  4240  setindel  4263  elirr  4266  en2lp  4278  zfregfr  4298  tfi  4305  zfinf2  4312  peano2  4318  peano5  4321  find  4322  raliunxp  4477  dmopab3  4548  issref  4707  asymref  4710  dffun7  4928  funcnv  4960  funcnvuni  4968  fnres  5015  fnopabg  5022  rexrnmpt  5310  dffo3  5314  acexmidlem2  5509  fz1sbc  8958  cbvrald  9927  bdcint  9997  bdcriota  10003  bj-axempty  10013  bj-indind  10056  bj-ssom  10060  peano5setOLD  10065  findset  10070  bj-nnord  10083  bj-inf2vn  10099  bj-inf2vn2  10100  bj-findis  10104  alsconv  10118