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  2817  ceqsralt  2827  rspct  2900  rspc  2901  rspcimdv  2908  rspc2gv  2919  ralab  2963  ralab2  2967  ralrab2  2968  reu2  2991  reu6  2992  reu3  2993  rmo4  2996  reu8  2999  rmo3f  3000  rmoim  3004  2reuswapdc  3007  2rmorex  3009  ra5  3118  rmo2ilem  3119  rmo3  3121  cbvralcsf  3187  dfss3  3213  dfss3f  3216  ssabral  3295  ss2rab  3300  rabss  3301  ssrab  3302  dfdif3  3314  ralunb  3385  reuss2  3484  rabeq0  3521  rabxmdc  3523  disj  3540  disj1  3542  r19.2m  3578  r19.2mOLD  3579  r19.3rm  3580  ralidm  3592  ralf0  3594  ralm  3595  ralsnsg  3703  ralsns  3704  unissb  3918  dfint2  3925  elint2  3930  elintrab  3935  ssintrab  3946  dfiin2g  3998  invdisj  4076  dftr5  4185  trint  4197  repizf2lem  4245  ordsucim  4592  ordunisuc2r  4606  setindel  4630  elirr  4633  en2lp  4646  zfregfr  4666  tfi  4674  zfinf2  4681  peano2  4687  peano5  4690  find  4691  raliunxp  4863  dmopab3  4936  issref  5111  asymref  5114  dffun7  5345  funcnv  5382  funcnvuni  5390  fnres  5440  fnopabg  5447  rexrnmpt  5780  dffo3  5784  acexmidlem2  6004  nfixpxy  6872  pw1dc0el  7081  isomnimap  7312  ismkvmap  7329  iswomnimap  7341  fz1sbc  10300  nnwosdc  12568  isprm2  12647  istopg  14681  cbvrald  16176  decidr  16184  bdcint  16264  bdcriota  16270  bj-axempty  16280  bj-indind  16319  bj-ssom  16323  findset  16332  bj-nnord  16345  bj-inf2vn  16361  bj-inf2vn2  16362  bj-findis  16366  alsconv  16478