Definition df-ral 2460

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

This definition is referenced by:  ralnex  2465  rexnalim  2466  dfrex2dc  2468  ralbida  2471  ralbidv2  2479  ralbid2  2481  ralbii2  2487  r2alf  2494  hbral  2506  hbra1  2507  nfra1  2508  nfraldw  2509  nfraldxy  2510  nfraldya  2512  r3al  2521  alral  2522  rsp  2524  rgen  2530  rgen2a  2531  ralim  2536  ralimi2  2537  ralimdaa  2543  ralimdv2  2547  ralrimi  2548  r19.21t  2552  ralrimd  2555  r19.21bi  2565  rexim  2571  r19.23t  2584  r19.26m  2608  r19.32r  2623  rabid2  2654  rabbi  2655  raleqf  2669  cbvralfw  2695  cbvralf  2697  cbvralvw  2708  cbvraldva2  2711  ralv  2755  ceqsralt  2765  rspct  2835  rspc  2836  rspcimdv  2843  rspc2gv  2854  ralab  2898  ralab2  2902  ralrab2  2903  reu2  2926  reu6  2927  reu3  2928  rmo4  2931  reu8  2934  rmo3f  2935  rmoim  2939  2reuswapdc  2942  2rmorex  2944  ra5  3052  rmo2ilem  3053  rmo3  3055  cbvralcsf  3120  dfss3  3146  dfss3f  3148  ssabral  3227  ss2rab  3232  rabss  3233  ssrab  3234  dfdif3  3246  ralunb  3317  reuss2  3416  rabeq0  3453  rabxmdc  3455  disj  3472  disj1  3474  r19.2m  3510  r19.2mOLD  3511  r19.3rm  3512  ralidm  3524  rgenm  3526  ralf0  3527  ralm  3528  ralsnsg  3630  ralsns  3631  unissb  3840  dfint2  3847  elint2  3852  elintrab  3857  ssintrab  3868  dfiin2g  3920  invdisj  3998  dftr5  4105  trint  4117  repizf2lem  4162  ordsucim  4500  ordunisuc2r  4514  setindel  4538  elirr  4541  en2lp  4554  zfregfr  4574  tfi  4582  zfinf2  4589  peano2  4595  peano5  4598  find  4599  raliunxp  4769  dmopab3  4841  issref  5012  asymref  5015  dffun7  5244  funcnv  5278  funcnvuni  5286  fnres  5333  fnopabg  5340  rexrnmpt  5660  dffo3  5664  acexmidlem2  5872  nfixpxy  6717  pw1dc0el  6911  isomnimap  7135  ismkvmap  7152  iswomnimap  7164  fz1sbc  10096  nnwosdc  12040  isprm2  12117  istopg  13502  cbvrald  14543  decidr  14551  bdcint  14632  bdcriota  14638  bj-axempty  14648  bj-indind  14687  bj-ssom  14691  findset  14700  bj-nnord  14713  bj-inf2vn  14729  bj-inf2vn2  14730  bj-findis  14734  alsconv  14830