Definition df-ral 2493

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

This definition is referenced by:  ralnex  2498  rexnalim  2499  dfrex2dc  2501  ralbida  2504  ralbidv2  2512  ralbid2  2514  ralbii2  2520  r2alf  2527  hbral  2539  hbra1  2540  nfra1  2541  nfraldw  2542  nfraldxy  2543  nfraldya  2545  r3al  2554  alral  2555  rsp  2557  rgen  2563  rgen2a  2564  ralim  2569  ralimi2  2570  ralimdaa  2576  ralimdv2  2580  ralrimi  2581  r19.21t  2585  ralrimd  2588  r19.21bi  2598  rexim  2604  r19.23t  2618  r19.26m  2642  r19.32r  2657  rabid2  2688  rabbi  2689  raleqf  2704  cbvralfw  2734  cbvralf  2736  cbvralvw  2749  cbvraldva2  2752  ralv  2797  ceqsralt  2807  rspct  2880  rspc  2881  rspcimdv  2888  rspc2gv  2899  ralab  2943  ralab2  2947  ralrab2  2948  reu2  2971  reu6  2972  reu3  2973  rmo4  2976  reu8  2979  rmo3f  2980  rmoim  2984  2reuswapdc  2987  2rmorex  2989  ra5  3098  rmo2ilem  3099  rmo3  3101  cbvralcsf  3167  dfss3  3193  dfss3f  3196  ssabral  3275  ss2rab  3280  rabss  3281  ssrab  3282  dfdif3  3294  ralunb  3365  reuss2  3464  rabeq0  3501  rabxmdc  3503  disj  3520  disj1  3522  r19.2m  3558  r19.2mOLD  3559  r19.3rm  3560  ralidm  3572  ralf0  3574  ralm  3575  ralsnsg  3683  ralsns  3684  unissb  3897  dfint2  3904  elint2  3909  elintrab  3914  ssintrab  3925  dfiin2g  3977  invdisj  4055  dftr5  4164  trint  4176  repizf2lem  4224  ordsucim  4569  ordunisuc2r  4583  setindel  4607  elirr  4610  en2lp  4623  zfregfr  4643  tfi  4651  zfinf2  4658  peano2  4664  peano5  4667  find  4668  raliunxp  4840  dmopab3  4913  issref  5087  asymref  5090  dffun7  5321  funcnv  5358  funcnvuni  5366  fnres  5416  fnopabg  5423  rexrnmpt  5751  dffo3  5755  acexmidlem2  5971  nfixpxy  6834  pw1dc0el  7041  isomnimap  7272  ismkvmap  7289  iswomnimap  7301  fz1sbc  10260  nnwosdc  12526  isprm2  12605  istopg  14638  cbvrald  16062  decidr  16070  bdcint  16150  bdcriota  16156  bj-axempty  16166  bj-indind  16205  bj-ssom  16209  findset  16218  bj-nnord  16231  bj-inf2vn  16247  bj-inf2vn2  16248  bj-findis  16252  alsconv  16359