Definition df-ral 2477

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

This definition is referenced by:  ralnex  2482  rexnalim  2483  dfrex2dc  2485  ralbida  2488  ralbidv2  2496  ralbid2  2498  ralbii2  2504  r2alf  2511  hbral  2523  hbra1  2524  nfra1  2525  nfraldw  2526  nfraldxy  2527  nfraldya  2529  r3al  2538  alral  2539  rsp  2541  rgen  2547  rgen2a  2548  ralim  2553  ralimi2  2554  ralimdaa  2560  ralimdv2  2564  ralrimi  2565  r19.21t  2569  ralrimd  2572  r19.21bi  2582  rexim  2588  r19.23t  2601  r19.26m  2625  r19.32r  2640  rabid2  2671  rabbi  2672  raleqf  2686  cbvralfw  2716  cbvralf  2718  cbvralvw  2730  cbvraldva2  2733  ralv  2777  ceqsralt  2787  rspct  2858  rspc  2859  rspcimdv  2866  rspc2gv  2877  ralab  2921  ralab2  2925  ralrab2  2926  reu2  2949  reu6  2950  reu3  2951  rmo4  2954  reu8  2957  rmo3f  2958  rmoim  2962  2reuswapdc  2965  2rmorex  2967  ra5  3075  rmo2ilem  3076  rmo3  3078  cbvralcsf  3144  dfss3  3170  dfss3f  3172  ssabral  3251  ss2rab  3256  rabss  3257  ssrab  3258  dfdif3  3270  ralunb  3341  reuss2  3440  rabeq0  3477  rabxmdc  3479  disj  3496  disj1  3498  r19.2m  3534  r19.2mOLD  3535  r19.3rm  3536  ralidm  3548  ralf0  3550  ralm  3551  ralsnsg  3656  ralsns  3657  unissb  3866  dfint2  3873  elint2  3878  elintrab  3883  ssintrab  3894  dfiin2g  3946  invdisj  4024  dftr5  4131  trint  4143  repizf2lem  4191  ordsucim  4533  ordunisuc2r  4547  setindel  4571  elirr  4574  en2lp  4587  zfregfr  4607  tfi  4615  zfinf2  4622  peano2  4628  peano5  4631  find  4632  raliunxp  4804  dmopab3  4876  issref  5049  asymref  5052  dffun7  5282  funcnv  5316  funcnvuni  5324  fnres  5371  fnopabg  5378  rexrnmpt  5702  dffo3  5706  acexmidlem2  5916  nfixpxy  6773  pw1dc0el  6969  isomnimap  7198  ismkvmap  7215  iswomnimap  7227  fz1sbc  10165  nnwosdc  12179  isprm2  12258  istopg  14178  cbvrald  15350  decidr  15358  bdcint  15439  bdcriota  15445  bj-axempty  15455  bj-indind  15494  bj-ssom  15498  findset  15507  bj-nnord  15520  bj-inf2vn  15536  bj-inf2vn2  15537  bj-findis  15541  alsconv  15640