Definition df-ral 2354

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 2349	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1284	. . . . 5 class 𝑥
6	5, 3	wcel 1434	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1283	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 103	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is referenced by:  ralnex  2359  rexnalim  2360  ralbida  2363  ralbidv2  2371  ralbii2  2377  r2alf  2384  hbral  2396  hbra1  2397  nfra1  2398  nfraldxy  2399  nfraldya  2401  r3al  2409  alral  2410  rsp  2412  rgen  2417  rgen2a  2418  ralim  2423  ralimi2  2424  ralimdaa  2429  ralimdv2  2432  ralrimi  2433  r19.21t  2437  ralrimd  2440  r19.21bi  2450  rexim  2456  r19.23t  2468  r19.26m  2489  r19.32r  2502  rabid2  2531  rabbi  2532  raleqf  2546  cbvralf  2572  cbvraldva2  2582  ralv  2617  ceqsralt  2627  rspct  2695  rspc  2696  rspcimdv  2703  rspc2gv  2713  ralab  2753  ralab2  2757  ralrab2  2758  reu2  2781  reu6  2782  reu3  2783  rmo4  2786  reu8  2789  rmoim  2792  2reuswapdc  2795  2rmorex  2797  ra5  2903  rmo2ilem  2904  rmo3  2906  cbvralcsf  2965  dfss3  2990  dfss3f  2992  ssabral  3066  ss2rab  3071  rabss  3072  ssrab  3073  ralunb  3154  reuss2  3251  rabeq0  3281  rabxmdc  3283  disj  3299  disj1  3301  r19.2m  3336  r19.3rm  3337  ralidm  3349  rgenm  3351  ralf0  3352  ralm  3353  ralsnsg  3438  ralsns  3439  unissb  3639  dfint2  3646  elint2  3651  elintrab  3656  ssintrab  3667  dfiin2g  3719  invdisj  3788  dftr5  3886  trint  3898  repizf2lem  3943  ordsucim  4252  ordunisuc2r  4266  setindel  4289  elirr  4292  en2lp  4305  zfregfr  4324  tfi  4331  zfinf2  4338  peano2  4344  peano5  4347  find  4348  raliunxp  4505  dmopab3  4576  issref  4737  asymref  4740  dffun7  4958  funcnv  4991  funcnvuni  4999  fnres  5046  fnopabg  5053  rexrnmpt  5342  dffo3  5346  acexmidlem2  5540  fz1sbc  9189  isprm2  10643  cbvrald  10749  decidr  10757  bdcint  10826  bdcriota  10832  bj-axempty  10842  bj-indind  10885  bj-ssom  10889  findset  10898  bj-nnord  10911  bj-inf2vn  10927  bj-inf2vn2  10928  bj-findis  10932  alsconv  10949