Definition df-ral 2533

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

This definition is referenced by:  ralnex  2538  rexnalim  2539  dfrex2dc  2541  ralbida  2544  ralbidv2  2552  ralbid2  2554  ralbii2  2560  r2alf  2567  hbral  2579  hbra1  2580  nfra1  2581  nfraldw  2582  nfraldxy  2583  nfraldya  2585  r3al  2594  alral  2595  rsp  2597  rgen  2603  rgen2a  2604  ralim  2609  ralimi2  2610  ralimdaa  2616  ralimdv2  2620  ralrimi  2621  r19.21t  2625  ralrimd  2628  r19.21bi  2638  rexim  2644  r19.23t  2658  r19.26m  2682  r19.32r  2697  rabid2  2729  rabbi  2730  raleqf  2745  cbvralfw  2775  cbvralf  2777  cbvralvw  2790  cbvraldva2  2793  ralv  2839  ceqsralt  2849  rspct  2922  rspc  2923  rspcimdv  2930  rspc2gv  2942  ralab  2986  ralab2  2990  ralrab2  2991  reu2  3014  reu6  3015  reu3  3016  rmo4  3019  reu8  3022  rmo3f  3023  rmoim  3027  2reuswapdc  3030  2rmorex  3032  ra5  3141  rmo2ilem  3142  rmo3  3144  cbvralcsf  3210  dfss3  3236  dfss3f  3240  ssabral  3319  ss2rab  3324  rabss  3325  ssrab  3326  dfdif3  3339  ralunb  3410  reuss2  3513  rabeq0  3552  disj  3573  disj1  3575  r19.2m  3614  r19.2mOLD  3615  r19.3rm  3616  ralidm  3628  ralf0  3630  ralm  3631  ralsnsg  3745  ralsns  3746  unissb  3963  dfint2  3970  elint2  3975  elintrab  3980  ssintrab  3991  dfiin2g  4043  invdisj  4121  dftr5  4230  trint  4242  repizf2lem  4296  ordsucim  4645  ordunisuc2r  4659  setindel  4683  elirr  4686  en2lp  4699  zfregfr  4719  tfi  4727  zfinf2  4734  peano2  4740  peano5  4743  find  4744  raliunxp  4919  dmopab3  4992  issref  5168  asymref  5171  dffun7  5402  funcnv  5440  funcnvuni  5448  fnres  5498  fnopabg  5505  rexrnmpt  5845  dffo3  5849  acexmidlem2  6075  nfixpxy  6992  pw1dc0el  7211  isomnimap  7470  ismkvmap  7487  iswomnimap  7499  fz1sbc  10484  nnwosdc  12797  isprm2  12876  istopg  15026  cbvrald  16733  decidr  16741  bdcint  16820  bdcriota  16826  bj-axempty  16836  bj-indind  16875  bj-ssom  16879  findset  16888  bj-nnord  16901  bj-inf2vn  16917  bj-inf2vn2  16918  bj-findis  16922  dfrals2  17038  alsralrex  17061  alsraln0m  17062