Definition df-ral 2421

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 2416	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1330	. . . . 5 class 𝑥
6	5, 3	wcel 1480	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1329	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 104	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

This definition is referenced by:  ralnex  2426  rexnalim  2427  dfrex2dc  2428  ralbida  2431  ralbidv2  2439  ralbii2  2445  r2alf  2452  hbral  2464  hbra1  2465  nfra1  2466  nfraldxy  2467  nfraldya  2469  r3al  2477  alral  2478  rsp  2480  rgen  2485  rgen2a  2486  ralim  2491  ralimi2  2492  ralimdaa  2498  ralimdv2  2502  ralrimi  2503  r19.21t  2507  ralrimd  2510  r19.21bi  2520  rexim  2526  r19.23t  2539  r19.26m  2563  r19.32r  2578  rabid2  2607  rabbi  2608  raleqf  2622  cbvralf  2648  cbvraldva2  2661  ralv  2703  ceqsralt  2713  rspct  2782  rspc  2783  rspcimdv  2790  rspc2gv  2801  ralab  2844  ralab2  2848  ralrab2  2849  reu2  2872  reu6  2873  reu3  2874  rmo4  2877  reu8  2880  rmo3f  2881  rmoim  2885  2reuswapdc  2888  2rmorex  2890  ra5  2997  rmo2ilem  2998  rmo3  3000  cbvralcsf  3062  dfss3  3087  dfss3f  3089  ssabral  3168  ss2rab  3173  rabss  3174  ssrab  3175  dfdif3  3186  ralunb  3257  reuss2  3356  rabeq0  3392  rabxmdc  3394  disj  3411  disj1  3413  r19.2m  3449  r19.2mOLD  3450  r19.3rm  3451  ralidm  3463  rgenm  3465  ralf0  3466  ralm  3467  ralsnsg  3561  ralsns  3562  unissb  3766  dfint2  3773  elint2  3778  elintrab  3783  ssintrab  3794  dfiin2g  3846  invdisj  3923  dftr5  4029  trint  4041  repizf2lem  4085  ordsucim  4416  ordunisuc2r  4430  setindel  4453  elirr  4456  en2lp  4469  zfregfr  4488  tfi  4496  zfinf2  4503  peano2  4509  peano5  4512  find  4513  raliunxp  4680  dmopab3  4752  issref  4921  asymref  4924  dffun7  5150  funcnv  5184  funcnvuni  5192  fnres  5239  fnopabg  5246  rexrnmpt  5563  dffo3  5567  acexmidlem2  5771  nfixpxy  6611  isomnimap  7009  ismkvmap  7028  fz1sbc  9876  isprm2  11798  istopg  12166  cbvrald  12995  decidr  13003  bdcint  13075  bdcriota  13081  bj-axempty  13091  bj-indind  13130  bj-ssom  13134  findset  13143  bj-nnord  13156  bj-inf2vn  13172  bj-inf2vn2  13173  bj-findis  13177  alsconv  13246