Definition df-ral 2515

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

This definition is referenced by:  ralnex  2520  rexnalim  2521  dfrex2dc  2523  ralbida  2526  ralbidv2  2534  ralbid2  2536  ralbii2  2542  r2alf  2549  hbral  2561  hbra1  2562  nfra1  2563  nfraldw  2564  nfraldxy  2565  nfraldya  2567  r3al  2576  alral  2577  rsp  2579  rgen  2585  rgen2a  2586  ralim  2591  ralimi2  2592  ralimdaa  2598  ralimdv2  2602  ralrimi  2603  r19.21t  2607  ralrimd  2610  r19.21bi  2620  rexim  2626  r19.23t  2640  r19.26m  2664  r19.32r  2679  rabid2  2710  rabbi  2711  raleqf  2726  cbvralfw  2756  cbvralf  2758  cbvralvw  2771  cbvraldva2  2774  ralv  2820  ceqsralt  2830  rspct  2903  rspc  2904  rspcimdv  2911  rspc2gv  2922  ralab  2966  ralab2  2970  ralrab2  2971  reu2  2994  reu6  2995  reu3  2996  rmo4  2999  reu8  3002  rmo3f  3003  rmoim  3007  2reuswapdc  3010  2rmorex  3012  ra5  3121  rmo2ilem  3122  rmo3  3124  cbvralcsf  3190  dfss3  3216  dfss3f  3219  ssabral  3298  ss2rab  3303  rabss  3304  ssrab  3305  dfdif3  3317  ralunb  3388  reuss2  3487  rabeq0  3524  rabxmdc  3526  disj  3543  disj1  3545  r19.2m  3581  r19.2mOLD  3582  r19.3rm  3583  ralidm  3595  ralf0  3597  ralm  3598  ralsnsg  3706  ralsns  3707  unissb  3923  dfint2  3930  elint2  3935  elintrab  3940  ssintrab  3951  dfiin2g  4003  invdisj  4081  dftr5  4190  trint  4202  repizf2lem  4251  ordsucim  4598  ordunisuc2r  4612  setindel  4636  elirr  4639  en2lp  4652  zfregfr  4672  tfi  4680  zfinf2  4687  peano2  4693  peano5  4696  find  4697  raliunxp  4871  dmopab3  4944  issref  5119  asymref  5122  dffun7  5353  funcnv  5391  funcnvuni  5399  fnres  5449  fnopabg  5456  rexrnmpt  5790  dffo3  5794  acexmidlem2  6014  nfixpxy  6885  pw1dc0el  7102  isomnimap  7335  ismkvmap  7352  iswomnimap  7364  fz1sbc  10330  nnwosdc  12609  isprm2  12688  istopg  14722  cbvrald  16384  decidr  16392  bdcint  16472  bdcriota  16478  bj-axempty  16488  bj-indind  16527  bj-ssom  16531  findset  16540  bj-nnord  16553  bj-inf2vn  16569  bj-inf2vn2  16570  bj-findis  16574  alsconv  16691