Definition df-ral 2490

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

This definition is referenced by:  ralnex  2495  rexnalim  2496  dfrex2dc  2498  ralbida  2501  ralbidv2  2509  ralbid2  2511  ralbii2  2517  r2alf  2524  hbral  2536  hbra1  2537  nfra1  2538  nfraldw  2539  nfraldxy  2540  nfraldya  2542  r3al  2551  alral  2552  rsp  2554  rgen  2560  rgen2a  2561  ralim  2566  ralimi2  2567  ralimdaa  2573  ralimdv2  2577  ralrimi  2578  r19.21t  2582  ralrimd  2585  r19.21bi  2595  rexim  2601  r19.23t  2614  r19.26m  2638  r19.32r  2653  rabid2  2684  rabbi  2685  raleqf  2699  cbvralfw  2729  cbvralf  2731  cbvralvw  2743  cbvraldva2  2746  ralv  2790  ceqsralt  2800  rspct  2871  rspc  2872  rspcimdv  2879  rspc2gv  2890  ralab  2934  ralab2  2938  ralrab2  2939  reu2  2962  reu6  2963  reu3  2964  rmo4  2967  reu8  2970  rmo3f  2971  rmoim  2975  2reuswapdc  2978  2rmorex  2980  ra5  3088  rmo2ilem  3089  rmo3  3091  cbvralcsf  3157  dfss3  3183  dfss3f  3186  ssabral  3265  ss2rab  3270  rabss  3271  ssrab  3272  dfdif3  3284  ralunb  3355  reuss2  3454  rabeq0  3491  rabxmdc  3493  disj  3510  disj1  3512  r19.2m  3548  r19.2mOLD  3549  r19.3rm  3550  ralidm  3562  ralf0  3564  ralm  3565  ralsnsg  3671  ralsns  3672  unissb  3882  dfint2  3889  elint2  3894  elintrab  3899  ssintrab  3910  dfiin2g  3962  invdisj  4040  dftr5  4149  trint  4161  repizf2lem  4209  ordsucim  4552  ordunisuc2r  4566  setindel  4590  elirr  4593  en2lp  4606  zfregfr  4626  tfi  4634  zfinf2  4641  peano2  4647  peano5  4650  find  4651  raliunxp  4823  dmopab3  4896  issref  5070  asymref  5073  dffun7  5303  funcnv  5340  funcnvuni  5348  fnres  5398  fnopabg  5405  rexrnmpt  5730  dffo3  5734  acexmidlem2  5948  nfixpxy  6811  pw1dc0el  7015  isomnimap  7246  ismkvmap  7263  iswomnimap  7275  fz1sbc  10225  nnwosdc  12404  isprm2  12483  istopg  14515  cbvrald  15798  decidr  15806  bdcint  15887  bdcriota  15893  bj-axempty  15903  bj-indind  15942  bj-ssom  15946  findset  15955  bj-nnord  15968  bj-inf2vn  15984  bj-inf2vn2  15985  bj-findis  15989  alsconv  16093